diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/table.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 301b6ed50..bd2aa6c91 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -603,8 +603,11 @@ let string_of_modfile mp = (* same as [string_of_modfile], but preserves the capital/uncapital 1st char *) let file_of_modfile mp = - let s0 = raw_string_of_modfile mp in - let s = string_of_modfile mp in + let s0 = match mp with + | MPfile f -> string_of_id (List.hd (repr_dirpath f)) + | _ -> assert false + in + let s = String.copy (string_of_modfile mp) in if s.[0] <> s0.[0] then s.[0] <- s0.[0]; s |