# HG changeset patch
# User Jan Vrany <jan.vrany@fit.cvut.cz>
# Date 1448273670 -3600
# Node ID 00ebb1b85f531afce5e4fadb8666d17dbfc038c1
# Parent  777f3813febc9b1be9b60b76c163fbc5abed7476
Fixed CI scripts on Windows

For an unknown reason, unzip on Windows reports status code 50
(presumably "the disk is (or was) full during extraction.") even
if there's plenty of space. To workaround this, simply ignore
status code 50 on Windows. Sigh.

diff -r 777f3813febc -r 00ebb1b85f53 ci/ci-common.sh
--- 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