bin/isatool
changeset 7971 023778c8a029
parent 3276 f8bf5e5c1641
child 9786 270ca580b880
equal deleted inserted replaced
7970:a15748c3b7e4 7971:023778c8a029
    67 do
    67 do
    68   TOOL=$DIR/$TOOLNAME
    68   TOOL=$DIR/$TOOLNAME
    69   [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
    69   [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
    70 done
    70 done
    71 
    71 
    72 fail "Unknown isabelle tool: $TOOLNAME"
    72 fail "Unknown Isabelle tool: $TOOLNAME"