--- 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