From c94e34d4e49e4fa0b570e77538b2fc7628ded16d Mon Sep 17 00:00:00 2001
From: "john.j.camilleri" <john.j.camilleri@chalmers.se>
Date: Fri, 23 Nov 2012 08:08:13 +0000
Subject: [PATCH] Minibar: add show/hide functions

---
 src/www/minibar/minibar.js | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/www/minibar/minibar.js b/src/www/minibar/minibar.js
index 10a469b6b..258de3078 100644
--- a/src/www/minibar/minibar.js
+++ b/src/www/minibar/minibar.js
@@ -57,6 +57,12 @@ function Minibar(server,opts) {
 	    menubar.appendChild(button("Help",bind(open_help,this)));
 	append_extra_buttons(extra,options);
     }
+    this.hide = function() {
+        this.minibar.style.display="none";
+    }
+    this.show = function() {
+        this.minibar.style.display="block";
+    }
 
     /* --- Minibar client state initialisation ------------------------------ */
     this.grammar=null;