equal
deleted
inserted
replaced
71 done |
71 done |
72 |
72 |
73 if [ "$PLATFORM" = x86-cygwin ]; then |
73 if [ "$PLATFORM" = x86-cygwin ]; then |
74 EXE="$ARCHIVE_DIR/contrib/x86-cygwin/Isabelle.exe" |
74 EXE="$ARCHIVE_DIR/contrib/x86-cygwin/Isabelle.exe" |
75 if [ -e "$EXE" ]; then |
75 if [ -e "$EXE" ]; then |
|
76 rm -f "$ISABELLE_HOME/Isabelle" |
76 cp "$EXE" "$ISABELLE_HOME/" |
77 cp "$EXE" "$ISABELLE_HOME/" |
77 chmod +x "$ISABELLE_HOME/Isabelle.exe" |
78 chmod +x "$ISABELLE_HOME/Isabelle.exe" |
78 else |
79 else |
79 fail "Missing $EXE" |
80 fail "Missing $EXE" |
80 fi |
81 fi |