# HG changeset patch
# User wenzelm
# Date 1522237581 -7200
# Node ID f69ea1a88c1affb0901519270e9061e40538c4f3
# Parent  b731a8d37131816a2f39dc44bbd9c4368fcdae1b
clarified handling of stdout vs. stderr: the cronjob should normally be silent;

diff -r b731a8d37131 -r f69ea1a88c1a Admin/cronjob/self_update
--- a/Admin/cronjob/self_update	Wed Mar 28 11:54:18 2018 +0200
+++ b/Admin/cronjob/self_update	Wed Mar 28 13:46:21 2018 +0200
@@ -10,6 +10,8 @@
 cd "$HOME/cronjob"
 mkdir -p run log
 
-hg -R isabelle pull "https://isabelle.in.tum.de/repos/isabelle" -q || echo "self_update pull failed"
-hg -R isabelle update -C -q || echo "self_update update failed"
-isabelle/bin/isabelle components -a || echo "self_update components failed"
+{
+  hg -R isabelle pull "https://isabelle.in.tum.de/repos/isabelle" || echo "self_update pull failed" >&2
+  hg -R isabelle update -C || echo "self_update update failed" >&2
+  isabelle/bin/isabelle components -a 2>&1 || echo "self_update components failed" >&2
+} > run/self_update.out