Admin/cronjob/crontab.vmnipkow17
author Thomas Lindae <thomas.lindae@in.tum.de>
Sun, 30 Jun 2024 15:29:44 +0200
changeset 81034 50082e028475
parent 80716 f3c9203d82c3
permissions -rw-r--r--
lsp: made margins synchronized;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
66995
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
     1
SHELL=/bin/bash
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
     2
MAILTO=wenzelm
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents:
diff changeset
     3
67765
968f6891be62 identify closer to main cronjob -- avoid diverging changeset versions;
wenzelm
parents: 66995
diff changeset
     4
20 00 * * *       $HOME/cronjob/plain_identify