aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorMaxime Dénès2017-08-29 13:09:37 +0200
committerMaxime Dénès2017-08-29 13:09:37 +0200
commit799d17738ebbae30a007b308998a669a9139cf1d (patch)
tree9a10365b80b5320938c0a7ef1e6e392b49f52fb4 /tools
parentef0450ded84d0fc27b5051baf94acfb6e541a7bf (diff)
parentaf6a390219de9eb1a91ffd9f5ca15a2d2253e978 (diff)
Merge PR #985: Fix coqdoc test-suite target on Windows.
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/index.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 8ba6156709..1bbf76490d 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -117,7 +117,7 @@ let find_module m =
if Hashtbl.mem local_modules m then
Local
else
- try External (Filename.concat (find_external_library m) m)
+ try External (find_external_library m ^ "/" ^ m)
with Not_found -> Unknown