diff options
| author | Son HO | 2022-09-22 16:25:47 +0200 |
|---|---|---|
| committer | GitHub | 2022-09-22 16:25:47 +0200 |
| commit | ba68c1ab4a7bd7817068d34d44fca38e4c547d90 (patch) | |
| tree | 90269db1d58a0fd299b5a9bf7149de5dd295b0cc /src | |
| parent | 0227077e343a6243a5c69dfb3eb07f50006eb5ea (diff) | |
Update src/Translate.ml
Diffstat (limited to '')
| -rw-r--r-- | src/Translate.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index fdd6d05f..25aff2b2 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -655,7 +655,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) m.declarations)) in - (* Register unique names for all the top-level types, functions and globals. + (* Register unique names for all the top-level types, globals and functions. * Note that the order in which we generate the names doesn't matter: * we just need to generate a mapping from identifier to name, and make * sure there are no name clashes. *) |