equal
deleted
inserted
replaced
8 source "$HOME/.bashrc" |
8 source "$HOME/.bashrc" |
9 |
9 |
10 cd "$HOME/cronjob" |
10 cd "$HOME/cronjob" |
11 mkdir -p run log |
11 mkdir -p run log |
12 |
12 |
13 hg -R isabelle pull "https://isabelle.in.tum.de/repos/isabelle" -q || echo "self_update pull failed" |
13 { |
14 hg -R isabelle update -C -q || echo "self_update update failed" |
14 hg -R isabelle pull "https://isabelle.in.tum.de/repos/isabelle" || echo "self_update pull failed" >&2 |
15 isabelle/bin/isabelle components -a || echo "self_update components failed" |
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 |
|
17 } > run/self_update.out |