diff --git a/Makefile b/Makefile new file mode 100644 index 00000000000..88c6c2cda2e --- /dev/null +++ b/Makefile @@ -0,0 +1,17 @@ +# +# Top level makefile for things not covered by cmake +# + +ifeq ($(VERBOSE),1) + Q = +else + Q = @ +endif + +MAKEFLAGS += --no-print-directory +export Q + +# Documentation targets +# --------------------------------------------------------------------------- +htmldocs: + $(Q)$(MAKE) -C doc htmldocs