equal
deleted
inserted
replaced
9 |
9 |
10 cd "$HOME/cronjob" |
10 cd "$HOME/cronjob" |
11 mkdir -p run log |
11 mkdir -p run log |
12 |
12 |
13 { |
13 { |
14 hg -R isabelle pull "https://isabelle.in.tum.de/repos/isabelle" || echo "self_update pull failed" >&2 |
14 hg -R isabelle pull "https://isabelle.sketis.net/repos/isabelle" || echo "self_update pull failed" >&2 |
15 hg -R isabelle update -C || echo "self_update update failed" >&2 |
15 hg -R isabelle update -C || echo "self_update update failed" >&2 |
16 isabelle/bin/isabelle components -a 2>&1 || echo "self_update components failed" >&2 |
16 isabelle/bin/isabelle components -a 2>&1 || echo "self_update components failed" >&2 |
17 } > run/self_update.out |
17 } > run/self_update.out |