author | paulson |
Tue, 26 Mar 2019 17:01:55 +0000 | |
changeset 69987 | e7648f104d6b |
parent 67766 | 603334230303 |
child 71297 | 9f2085c499a2 |
permissions | -rw-r--r-- |
64148 | 1 |
SHELL=/bin/bash |
67766
603334230303
consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents:
64352
diff
changeset
|
2 |
MAILTO=makarius |
64148 | 3 |
|
4 |
03 00 * * * $HOME/cronjob/self_update |
|
64352 | 5 |
17 00 * * * $HOME/cronjob/isabelle/Admin/cronjob/main -f > $HOME/cronjob/run/main.out 2>&1 || cat $HOME/cronjob/run/main.out |