adding /usr/local/bin/ to the PATH in git hooks, for compatibility wi…

…th Sourcetree
leanprover-community · Mar 31, 2019 · e851d3b · e851d3b
1 parent 5793330
commit e851d3b
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git a/scripts/post-checkout b/scripts/post-checkout
@@ -1,16 +1,15 @@
 #!/bin/sh
+export PATH=/usr/local/bin:$PATH
 export PATH=$HOME/.mathlib/bin:$PATH
 
 OLD_HEAD=$1
 NEW_HEAD=$2
 CHANGED_BRANCH=$3
 
 if [ "$CHANGED_BRANCH" -eq "1" ]; then
-    # hooks are sometimes run from git GUIs with a limited environment
-    # if python3 isn't available, we don't generate an error; just a message
     if /usr/bin/env python3 -c ""; then
-	echo "Trying to fetch cached olean"
-	cache-olean --fetch
+		echo "Trying to fetch cached olean"
+		cache-olean --fetch
     else
         echo "'env python3' failed; not running post-checkout hook"
     fi

diff --git a/scripts/post-commit b/scripts/post-commit
@@ -1,9 +1,12 @@
 #!/bin/sh
+export PATH=/usr/local/bin:$PATH
+export PATH=$HOME/.mathlib/bin:$PATH
+
 # hooks are sometimes run from git GUIs with a limited environment
 # if python3 isn't available, we don't generate an error; just a message
 if /usr/bin/env python3 -c ""; then
 	echo "Caching olean..."
-	$HOME/.mathlib/bin/cache-olean
+	cache-olean
 else
     echo "'env python3' failed; not running post-checkout hook"
 fi