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 "http://isabelle.in.tum.de/repos/isabelle" -q || echo "self_update pull failed" |
13 hg -R isabelle pull "http://bitbucket.org/isabelle_project/isabelle-release" -q || echo "self_update pull failed" |
14 hg -R isabelle update -C -q || echo "self_update update failed" |
14 hg -R isabelle update -C -q || echo "self_update update failed" |