diff options
| author | hallgren <hallgren@chalmers.se> | 2013-04-23 13:55:00 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2013-04-23 13:55:00 +0000 |
| commit | 1146b94685331341a2b16ad27ef76b5d7612cb3d (patch) | |
| tree | 77f33833e8a2a6e8145c1cbbc9bdb382b08d079e /src/www/minibar | |
| parent | 2639dc67b147edfa3c491a2de05eeb3648141de5 (diff) | |
gfse: add access to the syntax editor
via the minibar
Diffstat (limited to 'src/www/minibar')
| -rw-r--r-- | src/www/minibar/minibar.js | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/www/minibar/minibar.js b/src/www/minibar/minibar.js index fa572cfa8..a82c60198 100644 --- a/src/www/minibar/minibar.js +++ b/src/www/minibar/minibar.js @@ -92,6 +92,7 @@ Minibar.prototype.integrate_syntax_editor=function() { var languages=filter(not_all,minibar.translations.toLangs) var editor_options = { target: editor_target, + show_grammar_menu: minibar.grammars.length>1, show_startcat_menu: minibar.input.options.startcat_menu, initial: { grammar: minibar.grammar_menu.value, // hmm startcat: minibar.input.startcat_menu.value, // hmm |