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"