equal
deleted
inserted
replaced
8 source "$HOME/.bashrc" |
8 source "$HOME/.bashrc" |
9 |
9 |
10 LANG=C |
10 LANG=C |
11 |
11 |
12 REPOS_DIR="$HOME/cronjob/plain_identify_repos" |
12 REPOS_DIR="$HOME/cronjob/plain_identify_repos" |
13 ISABELLE_REPOS_SOURCE="https://isabelle.in.tum.de/repos/isabelle" |
13 ISABELLE_REPOS_SOURCE="https://isabelle.sketis.net/repos/isabelle" |
14 AFP_REPOS_SOURCE="https://isabelle.sketis.net/repos/afp-devel" |
14 AFP_REPOS_SOURCE="https://isabelle.sketis.net/repos/afp-devel" |
15 |
15 |
16 function setup_repos () |
16 function setup_repos () |
17 { |
17 { |
18 local NAME="$1" |
18 local NAME="$1" |