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,