blob: f4bf3650017bd9cf58718a67505c752e4c8eccc6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
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
|