From 146a9d73bd5ceff18e08d36d942dca874f388d5c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 11:42:56 +0100
Subject: Fix undefined SPHINX_DEPS when QUICK

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

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index 7ac710b8c9..4b2dd8ed4d 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -54,6 +54,7 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 
 doc: refman stdlib
 
+SPHINX_DEPS ?=
 ifndef QUICK
 SPHINX_DEPS := coq
 endif
-- 
cgit v1.2.3