Merge branch 'tor-github/pr/717'

2024-12-06 19:41:15 +01:00 · 2019-03-05 14:26:59 -05:00
parent f1890707cc 7f0516022b
commit db2e916afe
2 changed files with 35 additions and 10 deletions
@@ -0,0 +1,4 @@
+  o Minor features (developer tooling):
+    - Modify git pre-push hook script to disallow pushing branches other than
+      master, release-* and maint-* to origin remote. Implements feature
+      29532.