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 /isar/interface | |
| parent | 41113572f109f81db301aab9ed828cb60438c4c8 (diff) | |
isa: DEFAULT_FILES="Scratch.thy Scratch.ML";
Diffstat (limited to 'isar/interface')
| -rw-r--r-- | isar/interface | 4 |
1 files changed, 3 insertions, 1 deletions
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 |