diff --git a/Makefile b/Makefile
index 21b376fb71b107c60b261115127a73103485b317..3c55f27f9370a4d9fa19c162725807d3d05f3564 100644
--- a/Makefile
+++ b/Makefile
@@ -34,6 +34,9 @@ doc:
 	$(MAKE) -C user-doc
 	$(MAKE) -C developer-doc
 
+docs:
+	$(MAKE) doc
+
 # regtests
 check: src test
 	$(MAKE) -C regtest