1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Description: Allow local gpr options on the make command line.
Forwarded by private mail to report@adacore.com on 2018/6/11.
Author: Nicolas Boulenguez <nicolas@debian.org>
Forwarded: yes
--- a/Makefile
+++ b/Makefile
@@ -24,7 +24,10 @@
CONF_ARGS = $(TARGET_CONF) $(RTS_CONF)
-GPROPTS = $(CONF_ARGS) -XMODE=$(MODE) -XRUNTIME=$(RTS) -XPLATFORM=$(TARGET)
+# User may set this variable to pass more arguments to gpr* tools.
+USER_GPR_ARGS :=
+
+GPROPTS = $(CONF_ARGS) -XMODE=$(MODE) -XRUNTIME=$(RTS) -XPLATFORM=$(TARGET) $(USER_GPR_ARGS)
.PHONY: all clean targets install_clean install
|
