diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/www/minibar/minibar.html | 3 | ||||
| -rw-r--r-- | src/www/minibar/minibar_online.js | 3 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/www/minibar/minibar.html b/src/www/minibar/minibar.html index e3a6cbdf0..c729561cd 100644 --- a/src/www/minibar/minibar.html +++ b/src/www/minibar/minibar.html @@ -27,10 +27,11 @@ & <a href="http://www.grammaticalframework.org:41296/translate/">Translator</a>] </small> <small class=modtime> -HTML <!-- hhmts start -->Last modified: Wed Nov 21 15:50:29 CET 2012 <!-- hhmts end --> +HTML <!-- hhmts start -->Last modified: Fri Nov 23 16:07:35 CET 2012 <!-- hhmts end --> </small> <address> +<script type="text/JavaScript" src="../js/grammar_manager.js"></script> <script type="text/JavaScript" src="../js/support.js"></script> <script type="text/JavaScript" src="minibar.js"></script> <script type="text/JavaScript" src="minibar_input.js"></script> diff --git a/src/www/minibar/minibar_online.js b/src/www/minibar/minibar_online.js index c4bc61039..c5b1c1e5c 100644 --- a/src/www/minibar/minibar_online.js +++ b/src/www/minibar/minibar_online.js @@ -49,7 +49,8 @@ if(window.Editor) // Syntax editor loaded? } } minibar.minibar.style.display="none" // Hide the minibar - var editor=new Editor(server,editor_options) + var gm = new GrammarManager(server); + var editor=new Editor(gm,editor_options) } if(/^\?\/tmp\//.test(location.search)) { |