aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tools/coqdep_common.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 759b0cf967..4dcd10ece8 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -38,6 +38,7 @@ let is_dir_sep s i =
| "Unix" -> s.[i] = '/'
| "Cygwin" | "Win32" ->
let c = s.[i] in c = '/' || c = '\\' || c = ':'
+ | _ -> assert false
let (//) dirname filename =
let l = String.length dirname in