diff --git a/pull.sh b/pull.sh index 019661c..0cd463d 100755 --- a/pull.sh +++ b/pull.sh @@ -29,8 +29,11 @@ for directory in ../*; do log_git_pull "$directory" done +log_git_pull "$HOME"/git/lean4game/games/alexkontorovich/realanalysisgame log_git_pull "$HOME"/git/lean4game/games/djvelleman/stg4 +log_git_pull "$HOME"/git/lean4game/games/emilyriehl/reintroductiontoproofs log_git_pull "$HOME"/git/lean4game/games/hhu-adam/robo log_git_pull "$HOME"/git/lean4game/games/jadabouhawili/knightsandknaves-lean4game log_git_pull "$HOME"/git/lean4game/games/leanprover-community/nng4 log_git_pull "$HOME"/git/lean4game/games/trequetrum/lean4game-logic +log_git_pull "$HOME"/git/lean4game/games/zrtmrh/linearalgebragame