From 1ae6f0640e03d7375c5585c77fc6df9d1ab0630e Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Tue, 19 Sep 2000 09:44:04 +0000 Subject: isa: DEFAULT_FILES="Scratch.thy Scratch.ML"; --- isar/interface | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'isar/interface') diff --git a/isar/interface b/isar/interface index 97aa607f..7f323fdf 100644 --- a/isar/interface +++ b/isar/interface @@ -94,8 +94,10 @@ shift $(($OPTIND - 1)) if [ "$ISAR" = true ]; then KIND=isar + DEFAULT_FILES="Scratch.thy" else KIND=isa + DEFAULT_FILES="Scratch.thy Scratch.ML" fi @@ -104,7 +106,7 @@ fi FILES="$@" shift "$#" -[ -z "$FILES" ] && FILES="Scratch.thy" +[ -z "$FILES" ] && FILES="$DEFAULT_FILES" ## main -- cgit v1.2.3