Portability fix: 'if ! diff ...' is not always supported in sh.

diff --git a/Makefile.inc b/Makefile.inc
index dd724ba3fe1cf22ac74d16056f580cb6f11fadc0..aa01812cf7e657818cd3b060b17d25fef09da4e0 100644 (file)
--- a/Makefile.inc
+++ b/Makefile.inc
@@ -16,8 +16,10 @@ endef
        then \
          touch $(srcdir)/$@; \
        fi
-       if ! diff -q $< $(srcdir)/$@ > /dev/null; \
+       if diff $< $(srcdir)/$@ > /dev/null 2>&1; \
        then \
+         : ; \
+       else \
          rm $(srcdir)/$@; \
          cp $(srcdir)/$< $(srcdir)/$@; \
        fi