diff options
Diffstat (limited to 'plugins/extraction/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index a1e59e2a09..a27a9cf031 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -178,7 +178,6 @@ type language_descr = { (* Concerning the source file *) file_suffix : string; - capital_file : bool; (* should we capitalize filenames ? *) preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; pp_struct : ml_structure -> std_ppcmds; |