From 18f17ba857dbcdff789410e98f95dd30c6786021 Mon Sep 17 00:00:00 2001
From: hallgren <hallgren@chalmers.se>
Date: Thu, 9 Jun 2016 14:20:24 +0000
Subject: [PATCH] minibar: define grammar_list in config.js to restrict the
 grammar menu

minibar.html now reads config.js and if it defines grammar_list, only the
grammars listed there will show up in the grammar menu.
---
 src/www/minibar/minibar.html      | 3 ++-
 src/www/minibar/minibar_online.js | 2 ++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/www/minibar/minibar.html b/src/www/minibar/minibar.html
index 3eea85c22..b1382339e 100644
--- a/src/www/minibar/minibar.html
+++ b/src/www/minibar/minibar.html
@@ -27,11 +27,12 @@
 &amp; <a href="http://www.grammaticalframework.org:41296/translate/">Translator</a>]
 </small>
 <small class=modtime>
-HTML <!-- hhmts start -->Last modified: Mon May 18 17:31:07 CEST 2015 <!-- hhmts end -->
+HTML <!-- hhmts start -->Last modified: Thu Jun  9 16:13:26 CEST 2016 <!-- hhmts end -->
 </small>
 
 <div id="debug" class="hidden"></div>
 
+<script type="text/javascript" src="config.js"></script> <!-- optional -->
 <script type="text/JavaScript" src="../js/grammar_manager.js"></script>
 <script type="text/JavaScript" src="../js/support.js"></script>
 <script type="text/JavaScript" src="../js/localstorage.js"></script>
diff --git a/src/www/minibar/minibar_online.js b/src/www/minibar/minibar_online.js
index 0f35f4514..8ff10f7fb 100644
--- a/src/www/minibar/minibar_online.js
+++ b/src/www/minibar/minibar_online.js
@@ -7,6 +7,8 @@ var online_options={
   //grammar_list: ["Foods.pgf"], // leave undefined to get list from server
 }
 
+if(window.grammar_list) online_options.grammar_list=grammar_list
+
 var minibar_options= {
     show_abstract: true,
     show_trees: true,