ci/ci-common.sh
changeset 551 00ebb1b85f53
parent 549 8ad6734770cd
child 552 f79944e2bd85
--- a/ci/ci-common.sh	Mon Nov 09 00:38:23 2015 +0000
+++ b/ci/ci-common.sh	Mon Nov 23 11:14:30 2015 +0100
@@ -36,6 +36,14 @@
         *)
           ;;
       esac
+      # This is weird, but on Windows, sometimes I got
+      # exit code 50 from unzip even though there's plenty
+      # of space. To workaround, simply ignore it here, sigh.
+      if [ "$OS" == "Windows_NT" ]; then
+	if [ "$status" == "50" ]; then
+	  status=0
+	fi
+      fi	
       rm -f "$file"
     popd
   else