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 export LANG=C |
|
15 export HGPLAIN= |
|
16 |
14 "${HG:-hg}" -R isabelle pull "https://isabelle.sketis.net/repos/isabelle" || echo "self_update pull failed" >&2 |
17 "${HG:-hg}" -R isabelle pull "https://isabelle.sketis.net/repos/isabelle" || echo "self_update pull failed" >&2 |
15 "${HG:-hg}" -R isabelle update -C || echo "self_update update failed" >&2 |
18 "${HG:-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 |
19 isabelle/bin/isabelle components -a 2>&1 || echo "self_update components failed" >&2 |
17 } > run/self_update.out |
20 } > run/self_update.out |