Admin/cronjob/crontab.server
changeset 67766 603334230303
parent 64352 74ece0e491b6
child 71297 9f2085c499a2
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/cronjob/crontab.server	Sun Mar 04 15:10:11 2018 +0100
@@ -0,0 +1,5 @@
+SHELL=/bin/bash
+MAILTO=makarius
+
+03 00 * * *       $HOME/cronjob/self_update
+17 00 * * *       $HOME/cronjob/isabelle/Admin/cronjob/main -f > $HOME/cronjob/run/main.out 2>&1 || cat $HOME/cronjob/run/main.out