equal
deleted
inserted
replaced
3 # Author: Makarius |
3 # Author: Makarius |
4 # |
4 # |
5 # Isabelle shell functions, with on-demand re-initialization for |
5 # Isabelle shell functions, with on-demand re-initialization for |
6 # non-interactive bash processess. NB: bash shell functions are not portable |
6 # non-interactive bash processess. NB: bash shell functions are not portable |
7 # and may be dropped by aggressively POSIX-conformant versions of /bin/sh. |
7 # and may be dropped by aggressively POSIX-conformant versions of /bin/sh. |
|
8 |
|
9 unset CDPATH |
8 |
10 |
9 if type splitarray >/dev/null 2>/dev/null |
11 if type splitarray >/dev/null 2>/dev/null |
10 then |
12 then |
11 : |
13 : |
12 else |
14 else |