diff options
| author | hallgren <hallgren@chalmers.se> | 2010-09-10 11:03:46 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2010-09-10 11:03:46 +0000 |
| commit | e13e47be8afaf1ce888ff9098cd09699bec34ffd (patch) | |
| tree | cf14c4f9323a3fb52ac73eb7a07724302104e9d2 /src/runtime/javascript/editor.html | |
| parent | 46da64cc7268a4a1d29675fd2ecce1e8fe113ae5 (diff) | |
minibar: default input language is now the user's preferred language, if possible
This is implemented using the userLanguage field in the grammar info output by
pgf-server.
Diffstat (limited to 'src/runtime/javascript/editor.html')
0 files changed, 0 insertions, 0 deletions