diff options
| author | Hugo Herbelin | 2019-04-27 12:11:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-27 12:11:45 +0200 |
| commit | fb400d6081f67b628d7627bc85e460d779e72dcd (patch) | |
| tree | 1c6da1ae31ca7290b826de436b6c21a740700870 | |
| parent | ae4239d6a5f4afcd9b7321dba790ffd4a64994a1 (diff) | |
Amending CYGWIN fix in 63e7fb56923 so that it does not add a warning on MacOS.
Indeed, MacOS has a BSD uname and BSD uname does not support the -o option.
Based on the following resources about uname compatility:
https://stackoverflow.com/questions/3466166/how-to-check-if-running-in-cygwin-mac-or-linux
https://en.wikipedia.org/wiki/Uname
| -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 |