pull.sh : Quiter output and can now add custom directories to pull
This commit is contained in:
		
							
								
								
									
										22
									
								
								pull.sh
									
									
									
									
									
								
							
							
						
						
									
										22
									
								
								pull.sh
									
									
									
									
									
								
							| @@ -9,18 +9,28 @@ __r__(){ | ||||
| 	done | ||||
| } | ||||
|  | ||||
| cd .. | ||||
|  | ||||
| for d in *; do | ||||
| 	cd "$d" || continue | ||||
| log_git_pull(){ | ||||
| 	directory="$1" | ||||
| 	test ! -d "$directory" && return | ||||
| 	cd "$directory" | ||||
|  | ||||
| 	PULL_LOG=$(script -q /dev/null -c 'git pull') | ||||
| 	if [ "$PULL_LOG" != "$(env printf 'Already up to date.\r\n')" ]; then | ||||
| 		env printf "┌$(__r__ 40 ─)┐\n" | ||||
| 		env printf "│ %-38s │\n" "$d" | ||||
| 		env printf "│ %-38s │\n" "$directory" | ||||
| 		env printf "└$(__r__ 40 '─')┘\n" | ||||
| 		echo "$PULL_LOG" | ||||
| 	fi | ||||
|  | ||||
| 	cd .. | ||||
| 	cd - >> /dev/null | ||||
| } | ||||
|  | ||||
| for directory in ../*; do | ||||
| 	log_git_pull "$directory" | ||||
| done | ||||
|  | ||||
| log_git_pull "$HOME"/git/lean4game/games/djvelleman/stg4 | ||||
| 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 | ||||
|   | ||||
		Reference in New Issue
	
	Block a user