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