ci/ci-common.sh
changeset 551 00ebb1b85f53
parent 549 8ad6734770cd
child 552 f79944e2bd85
equal deleted inserted replaced
550:777f3813febc 551:00ebb1b85f53
    34           status=0
    34           status=0
    35           ;;
    35           ;;
    36         *)
    36         *)
    37           ;;
    37           ;;
    38       esac
    38       esac
       
    39       # This is weird, but on Windows, sometimes I got
       
    40       # exit code 50 from unzip even though there's plenty
       
    41       # of space. To workaround, simply ignore it here, sigh.
       
    42       if [ "$OS" == "Windows_NT" ]; then
       
    43 	if [ "$status" == "50" ]; then
       
    44 	  status=0
       
    45 	fi
       
    46       fi	
    39       rm -f "$file"
    47       rm -f "$file"
    40     popd
    48     popd
    41   else
    49   else
    42     echo "Skipped $directory (already present)"
    50     echo "Skipped $directory (already present)"
    43   fi
    51   fi