diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep_common.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 235aa30745..e8d189ad97 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -50,7 +50,7 @@ let rec get_extension f = function let basename_noext filename = let fn = Filename.basename filename in - try Filename.chop_extension fn with _ -> fn + try Filename.chop_extension fn with Invalid_argument _ -> fn (** ML Files specified on the command line. In the entries: - the first string is the basename of the file, without extension nor |