bin/isabelle
changeset 3118 24dae6222579
parent 3054 c16029f41ad9
child 3183 537f7281d42c
--- a/bin/isabelle	Tue May 06 15:24:41 1997 +0200
+++ b/bin/isabelle	Tue May 06 15:27:35 1997 +0200
@@ -148,8 +148,8 @@
     OUTFILE="$OUTPUT"
     ;;
   *)
-    mkdir -p "$ISABELLE_OUTPUT_DIR"
-    OUTFILE="$ISABELLE_OUTPUT_DIR/$OUTPUT"
+    mkdir -p "$ISABELLE_OUTPUT"
+    OUTFILE="$ISABELLE_OUTPUT/$OUTPUT"
     ;;
 esac