lib/scripts/isa-emacs
changeset 9794 2be239143d42
parent 9789 7e5e6c47c0b5
child 10512 d34192966cd8
--- a/lib/scripts/isa-emacs	Fri Sep 01 19:40:57 2000 +0200
+++ b/lib/scripts/isa-emacs	Fri Sep 01 19:42:11 2000 +0200
@@ -84,12 +84,12 @@
 [ "$INITFILE" = false ] && ARGS="$ARGS -q"
 
 
-ARGS="$ARGS -l \"$ISAMODE_HOME/elisp/isa-site.el\""
+ARGS="$ARGS -l $ISAMODE_HOME/elisp/isa-site.el"
 
 for FILE in "$ISABELLE_HOME/etc/isa-settings.el" \
     "$ISABELLE_HOME_USER/etc/isa-settings.el"
 do
-  [ -f "$FILE" ] && ARGS="$ARGS -l \"$FILE\""
+  [ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
 done
 
 ARGS="$ARGS -f isabelle"