equal
deleted
inserted
replaced
74 ## main |
74 ## main |
75 |
75 |
76 [ -f "$FILE" ] || fail "Bad file: $FILE" |
76 [ -f "$FILE" ] || fail "Bad file: $FILE" |
77 |
77 |
78 if [ -n "$CLEAN" ]; then |
78 if [ -n "$CLEAN" ]; then |
79 PRIVATE_FILE="$ISABELLE_TMP_PREFIX/"$$"$FILE" |
79 PRIVATE_FILE="$ISABELLE_TMP/"$(basename "$FILE") |
80 mv "$FILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE" |
80 mv "$FILE" "$PRIVATE_FILE" ##|| fail "Cannot move file: $FILE" |
81 view "$PRIVATE_FILE" |
81 view "$PRIVATE_FILE" |
82 rm -f "$PRIVATE_FILE" |
82 rm -f "$PRIVATE_FILE" |
83 else |
83 else |
84 view "$FILE" |
84 view "$FILE" |
85 fi |
85 fi |