changeset 73705 | ac07f6be27ea |
parent 64498 | bb29e6849a28 |
child 74034 | d6ae3a7d9cb0 |
73704:7c7a59b76528 | 73705:ac07f6be27ea |
---|---|
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # DESCRIPTION: start the main Isabelle cronjob |
3 # DESCRIPTION: start the main Isabelle cronjob |
4 |
4 |
5 unset CDPATH |
|
5 THIS="$(cd "$(dirname "$0")"; pwd)" |
6 THIS="$(cd "$(dirname "$0")"; pwd)" |
6 |
7 |
7 source "$HOME/.bashrc" |
8 source "$HOME/.bashrc" |
8 |
9 |
9 export ISABELLE_IDENTIFIER="cronjob" |
10 export ISABELLE_IDENTIFIER="cronjob" |