diff options
Diffstat (limited to 'src/runtime')
| -rw-r--r-- | src/runtime/javascript/minibar/phrasebook.html | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/runtime/javascript/minibar/phrasebook.html b/src/runtime/javascript/minibar/phrasebook.html index 29321582a..19572b1cf 100644 --- a/src/runtime/javascript/minibar/phrasebook.html +++ b/src/runtime/javascript/minibar/phrasebook.html @@ -6,8 +6,9 @@ <script type="text/JavaScript" src="minibar.js"></script> <script type="text/JavaScript"> var phrasebook_options={ - server: "http://localhost:41296", +// server: "http://localhost:41296", // server: "http://tournesol.cs.chalmers.se:41296", + server: "http://www.grammaticalframework.org:41296", grammar_list: ["Phrasebook.pgf"], delete_button_text: "Del" } |