From 1b9588773387109753218a6395c77014b56bd8ea Mon Sep 17 00:00:00 2001
From: Xiretza <xiretza@xiretza.xyz>
Date: Sun, 24 May 2020 11:23:55 +0200
Subject: [PATCH 4/5] Honour GPRBUILD_FLAGS= in cli/Makefile

---
 cli/Makefile | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/cli/Makefile b/cli/Makefile
index 3b0630d8ef..8c6218cf5a 100644
--- a/cli/Makefile
+++ b/cli/Makefile
@@ -1,8 +1,9 @@
 GPRBUILD=gprbuild
 GPRCLEAN=gprclean
+GPRBUILD_FLAGS=
 
 all default:
-	$(GPRBUILD) -p -Pcli
+	$(GPRBUILD) $(GPRBUILD_FLAGS) -p -Pcli
 
 clean:
-	$(GPRCLEAN) -q -r -Pcli
+	$(GPRCLEAN) $(GPRBUILD_FLAGS) -q -r -Pcli
-- 
2.26.2