lib/Tools/display
changeset 15223 e669fb5b0f5a
parent 15218 39747a9e3c37
child 15703 727ef1b8b3ee
equal deleted inserted replaced
15222:2406fd8a5c30 15223:e669fb5b0f5a
    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