From 99ee01902770444337f69984f0d077be809ae322 Mon Sep 17 00:00:00 2001
From: Jonathan Wilkes <jon.w.wilkes@gmail.com>
Date: Fri, 3 Jun 2016 23:25:41 -0400
Subject: [PATCH] port cf4838aecd6cd3f389fdc7eff0496947e50311e4 from Pd-l2ork:
 hopefully improved building of flext library on older Ubuntu systems (e.g.
 12.04 32-bit)

---
 externals/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/externals/Makefile b/externals/Makefile
index 2e9bcf10c..ed1f99509 100644
--- a/externals/Makefile
+++ b/externals/Makefile
@@ -474,7 +474,7 @@ flatgui_clean:
 # FLEXT and FLEXT externals
 flext:
 	cd $(externals_src)/grill/trunk/flext && \
-	./bootstrap.sh && \
+	./bootstrap.sh || ./bootstrap.sh && \
 	./build.sh pd gcc build && \
 	./build.sh pd gcc build && \
 	./build.sh pd gcc build && \
-- 
GitLab