diff options
| author | Enrico Tassi | 2019-03-04 22:42:13 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-04 22:42:13 +0100 |
| commit | b0d35837ff193b66ba37355093b2227f2b1be1ac (patch) | |
| tree | 406ece20400cc39c9248719f8d8c114e6a34f0e5 /Makefile.build | |
| parent | 78b3b96d1ca2c2811cee2ca4202c154177d943a2 (diff) | |
| parent | 1a9f134e5ce7132ea38a6c73755e5773c4361aea (diff) | |
Merge PR #9687: Cleanup exported variables in Makefile.build
Reviewed-by: gares
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index e348b2b9b8..8b989f161a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -11,6 +11,9 @@ # This makefile is normally called by the main Makefile after setting # some variables. +# Cleanup environment (avoids filling it up) +unexport $(COQ_EXPORTED) + ########################################################################### # User-customizable variables ########################################################################### @@ -859,6 +862,18 @@ $(VDFILE).d: $(D_DEPEND_BEFORE_SRC) $(VFILES) $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT ########################################################################### + +# Useful to check that the exported variables are within the win32 limits + +printenv-real: + @env + @echo + @echo -n "Maxsize (win32 limit is 8k) : " + @env | wc -L + @echo -n "Total (win32 limit is 32k) : " + @env | wc -m + + # To speed-up things a bit, let's dissuade make to attempt rebuilding makefiles Makefile $(wildcard Makefile.*) config/Makefile : ; @@ -873,5 +888,5 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # For emacs: # Local Variables: -# mode: makefile +# mode: makefile-gmake # End: |