diff options
| author | Vincent Laporte | 2019-04-29 12:38:51 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-29 12:38:51 +0000 |
| commit | f08dacb28213f7da273d6594b317848dd5d776a8 (patch) | |
| tree | 5f92e422f5554eee56c916d72d71c7ceef6a495a | |
| parent | 530d72a251038f31e5dfe9d3b982ca744df01e59 (diff) | |
| parent | fb400d6081f67b628d7627bc85e460d779e72dcd (diff) | |
Merge PR #10007: Amending sphinx-on-windows fix in #9819 so that it does not trigger a warning on MacOS X (and other BSD systems).
Ack-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: vbgl
| -rw-r--r-- | Makefile.doc | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.doc b/Makefile.doc index e89a20393c..23aa66a1b8 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -31,8 +31,8 @@ DVIPS:=dvips HTMLSTYLE:=coqremote # Sphinx-related variables -OSNAME:=$(shell uname -o) -ifeq ($(OSNAME),Cygwin) +OSNAME:=$(shell uname -s) +ifeq ($(findstring CYGWIN,$(OSNAME)),CYGWIN) WIN_CURDIR:=$(shell cygpath -w $(CURDIR)) SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)" else |