proper spelling of JEDIT_JAVA_OPTIONS;
authorwenzelm
Fri, 19 Dec 2008 23:54:24 +0100
changeset 34409 e61e2ab1f6f7
parent 34408 ad7b6c4813c8
child 34410 f2644d2a3e8e
proper spelling of JEDIT_JAVA_OPTIONS; no extra quoting of FILES;
src/Tools/jEdit/dist-template/interface
--- a/src/Tools/jEdit/dist-template/interface	Fri Dec 19 23:11:08 2008 +0100
+++ b/src/Tools/jEdit/dist-template/interface	Fri Dec 19 23:54:24 2008 +0100
@@ -2,6 +2,8 @@
 #
 # Isabelle/jEdit interface wrapper
 
+set -x
+
 ## diagnostics
 
 usage()
@@ -11,7 +13,7 @@
   echo
   echo "  Options are:"
   echo "    -J OPTION    add JVM runtime option"
-  echo "                 (default JEDIT_JAVE_OPTIONS=$JEDIT_JAVE_OPTIONS)"
+  echo "                 (default JEDIT_JAVA_OPTIONS=$JEDIT_JAVA_OPTIONS)"
   echo "    -j OPTION    add jEdit runtime option"
   echo "                 (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
   echo "    -l NAME      logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
@@ -72,7 +74,7 @@
   FILES="isabelle:$HOME/Scratch.thy"
 else
   while [ "$#" -gt 0 ]; do
-    FILES="$FILES 'isabelle:$1'"
+    FILES="$FILES isabelle:$1"
     shift
   done
 fi