equal
deleted
inserted
replaced
74 echo 1>&2 "Failed to determine hardware and operating system type!" |
74 echo 1>&2 "Failed to determine hardware and operating system type!" |
75 exit 2 |
75 exit 2 |
76 fi |
76 fi |
77 |
77 |
78 #Isabelle distribution identifier -- filled in automatically! |
78 #Isabelle distribution identifier -- filled in automatically! |
79 ISABELLE_ID="8f4a332500e4" |
79 ISABELLE_ID="" |
80 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER="Isabelle2014" |
80 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER="Isabelle2014-Isac" |
81 |
81 |
82 #sometimes users put strange things in here ... |
82 #sometimes users put strange things in here ... |
83 unset ENV |
83 unset ENV |
84 unset BASH_ENV |
84 unset BASH_ENV |
85 |
85 |