summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-09 17:26:46 +0100
committerSon Ho2022-02-09 17:26:46 +0100
commitb6b77b38a16a102d3ccbc8bfad5a81a04eb3643d (patch)
tree9b92f74823373f2db22148a9bb06414990619843
parenta1d87256670b165de8079dd99b30bc837a8a4ff2 (diff)
Make a minor modification
Diffstat (limited to '')
-rw-r--r--src/Translate.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Translate.ml b/src/Translate.ml
index 7247279a..82b9f9cc 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -592,7 +592,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config)
let types_module = module_name ^ ".Types" in
let types_config = { base_gen_config with extract_types = true } in
extract_file types_config gen_ctx types_filename m.M.name types_module
- ": types definitions" [] [];
+ ": type definitions" [] [];
(* Extract the template clauses *)
(if