Add a do-nothing install-docs rule in ext-core/ when LATEX_DOCS=NO

diff --git a/docs/ext-core/Makefile b/docs/ext-core/Makefile
index 42c9a8f..cf1c28f 100644 (file)
--- a/docs/ext-core/Makefile
+++ b/docs/ext-core/Makefile
@@ -9,6 +9,7 @@ install-docs:
        cp core.pdf $(docdir)/ext-core/
 else
 all:
+install-docs:
 endif
 
 #      General makefile for Latex stuff