diff options
| -rwxr-xr-x | bin/reproducible_build.sh | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/bin/reproducible_build.sh b/bin/reproducible_build.sh index 21ad9b0e..8b540f46 100755 --- a/bin/reproducible_build.sh +++ b/bin/reproducible_build.sh @@ -14,9 +14,8 @@ common_init "$@" set -e exit_early_if_debian_is_broken() { - # disable everything until #827724 is fixed - # (it would be very nice to query udd to see if this bug is fixed and then automatically enable again…) - if [ "$ARCH" = "armhf" ] ; then + # debian is fine, thanks + if false && [ "$ARCH" = "armhf" ] ; then echo -n "temporarily stopping the builds on armhf due to #827724… sleeping 12h now…" for i in $(seq 1 12) ; do sleep 1h |