From 4bb8c9cf4ea4bc2ddb26aa1c02dee9a09b1a7d92 Mon Sep 17 00:00:00 2001
From: Giovanni Bussi <giovanni.bussi@gmail.com>
Date: Fri, 12 Sep 2014 16:18:22 +0200
Subject: [PATCH] Allow "make docs" besides "make doc"

(Asked by GT)
---
 Makefile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Makefile b/Makefile
index 21b376fb7..3c55f27f9 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
-- 
GitLab