aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2013-12-20 18:22:39 +0100
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2013-12-20 18:22:39 +0100
commit1e32ea82502c9ad8a0046d4dfe326f9a2e035101 (patch)
tree9493797f6326059f9608505b21a829aec6ee00cc /tools
parentde37a370a81c976aec56f25b2d7ddfa0dbad9145 (diff)
Warning removal
Diffstat (limited to 'tools')
-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 759b0cf96..4dcd10ece 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