diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-06-21 17:46:00 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-21 17:46:00 +0200 |
commit | 4a3697da7be172c1559588d326a2f02c80bb98e9 (patch) | |
tree | e19052e708a1950431f30d80e0f2716b89a0a1e2 | |
parent | 41cf6afdb70b073838bd2a1e71f76c600e03c006 (diff) | |
parent | 5808915bcb5f9800727cc10e5232c8983e1842bd (diff) |
Merge PR #7815: On cygwin, pass the filename in a format that coqdoc understands.
-rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index cedd60d3b..57adcb287 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -20,6 +20,7 @@ lexer. """ import os +import platform from tempfile import mkstemp from subprocess import check_output @@ -36,6 +37,9 @@ def coqdoc(coq_code, coqdoc_bin=None): """Get the output of coqdoc on coq_code.""" coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc") fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") + if platform.system().startswith("CYGWIN"): + # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..." + filename = check_output(["cygpath", "-w", filename]).decode("utf-8").strip() try: os.write(fd, COQDOC_HEADER.encode("utf-8")) os.write(fd, coq_code.encode("utf-8")) |