From 63e7fb56923990d464278840f72b731997b20b01 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 22 Mar 2019 21:44:51 -0700
Subject: Fix make sphinx failure

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

diff --git a/Makefile.doc b/Makefile.doc
index 5ac3ecb63d..e89a20393c 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -31,7 +31,13 @@ DVIPS:=dvips
 HTMLSTYLE:=coqremote
 
 # Sphinx-related variables
+OSNAME:=$(shell uname -o)
+ifeq ($(OSNAME),Cygwin)
+WIN_CURDIR:=$(shell cygpath -w $(CURDIR))
+SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)"
+else
 SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(CURDIR)"
+endif
 SPHINXOPTS= -j4
 SPHINXWARNERROR ?= 1
 ifeq ($(SPHINXWARNERROR),1)
-- 
cgit v1.2.3