From 8e0c968d375aa1cd9ed02d474682f90e99df7f7f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Aug 2017 11:16:06 +0200
Subject: Prevent warning about DSTROOT being undefined.

---
 tools/CoqMakefile.in | 4 ++--
 1 file 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
 
-- 
cgit v1.2.3