Add a --ignore-failure flag to push-all script

[ghc-hetmet.git] / push-all

diff --git a/push-all b/push-all
index 014c4b0..a5c2062 100644 (file)
--- a/push-all
+++ b/push-all
@@ -75,6 +75,9 @@ sub main {
             if ($arg eq "-q") {
                 $verbose = 0;
             }
+            elsif ($arg eq "--ignore-failure") {
+                $ignore_failure = 1;
+            }
             elsif ($arg eq "--checked-out") {
                 $checked_out = 1;
             }