diff options
author | Makarius Wenzel <makarius@sketis.net> | 2000-09-19 09:44:04 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2000-09-19 09:44:04 +0000 |
commit | 1ae6f0640e03d7375c5585c77fc6df9d1ab0630e (patch) | |
tree | 57d8700a90d1588fe3ff3482c6f5a48c28eccf0f | |
parent | 41113572f109f81db301aab9ed828cb60438c4c8 (diff) |
isa: DEFAULT_FILES="Scratch.thy Scratch.ML";
-rw-r--r-- | isa/interface | 4 | ||||
-rw-r--r-- | isar/interface | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/isa/interface b/isa/interface index 97aa607f..7f323fdf 100644 --- a/isa/interface +++ b/isa/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 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 |