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