diff --git a/Makefile b/Makefile index 2c8f42a2daac121b3072e181e9de1e2a5bc2b11d..b89a852a753a78e05e707727e2bca13196bf32d9 100644 --- a/Makefile +++ b/Makefile @@ -1071,9 +1071,9 @@ releasenotes: html: $(ROOTEXE) changelog releasenotes ifneq ($(USECONFIG),FALSE) - if [ "x`which root.exe`" != "x$(DESTDIR)$(BINDIR)/root.exe" ]; then \ - echo 'ERROR: available root.exe is '`which root.exe`; \ - echo ' should instead be $(DESTDIR)$(BINDIR)/root.exe'; \ + @if [ "x`which root.exe`" != "x$(DESTDIR)$(BINDIR)/root.exe" ] \ + || [ "`which root.exe`" -ot "bin/root.exe" ]; then \ + echo 'ERROR: root.exe has not been installed by this build.'; \ echo ' Run "make install" before running "make html".'; \ exit 1; \ fi