diff options
| author | Guillaume Melquiond | 2017-08-22 11:16:06 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-08-22 11:29:32 +0200 |
| commit | 8e0c968d375aa1cd9ed02d474682f90e99df7f7f (patch) | |
| tree | f0c479de937f1c2e4a20fe02d2de750bd061a552 | |
| parent | 325890a83a2b073d9654b5615c585cd65a376fbd (diff) | |
Prevent warning about DSTROOT being undefined.
| -rw-r--r-- | tools/CoqMakefile.in | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 9f891afe53..5c6e2b4cbc 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -199,8 +199,8 @@ else TIMING_ARG= endif -# Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not) -ifneq "$(DSTROOT)" "" +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT DESTDIR := $(DSTROOT) endif |