From cb2ee2d949899a897022894b750afd1f3d2eb478 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 5 Nov 2018 19:37:11 +0100
Subject: Integrate plugin tutorial after code import

---
 Makefile.doc | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index 9e6ec4955a..48cdcebddb 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -89,6 +89,10 @@ stdlib: \
 full-stdlib: \
   doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf
 
+.PHONY: plugin-tutorial
+plugin-tutorial: states tools
+	+$(MAKE) COQBIN=$(PWD)/bin/ -C $(PLUGINTUTO)
+
 ######################################################################
 ### Implicit rules
 ######################################################################
-- 
cgit v1.2.3