bin/isabelle
changeset 42124 7519c7c33017
parent 42077 96c50a4210a2
child 48858 86816c61b5ca
     1.1 --- a/bin/isabelle	Sat Mar 26 16:10:22 2011 +0100
     1.2 +++ b/bin/isabelle	Sat Mar 26 16:21:41 2011 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  do
     1.5    TOOL="$DIR/$TOOLNAME"
     1.6    case "$TOOL" in
     1.7 -    *~) ;;
     1.8 +    *~ | *.orig) ;;
     1.9      *) [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@" ;;
    1.10    esac
    1.11  done