Learn more about these different git repos.
Other Git URLs
7b22aa5
@@ -9,6 +9,10 @@
set -e
+ echo "============== ENVIRONMENT ============="
+ /usr/bin/env
+ echo "============== END ENVIRONMENT ============="
+
if [ -n "$REPO" -a -n "$BRANCH" ]; then
git remote rm proposed || true
git gc --auto
Pull-Request has been merged by pingou