summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-04-04 11:00:23 +0200
committerSon Ho2024-04-04 11:00:23 +0200
commitf58161f23ccb4bff2080a7c63105d80777c33362 (patch)
tree9cfb108c57285b0a254b71fc49f7e8d8cc5cb0b9
parenteae7ce912c8bae44f98e1d489aba5618c0029bd2 (diff)
Update a comment
Diffstat (limited to '')
-rw-r--r--compiler/ExtractBase.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index d760ab1e..f8d3cd96 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -268,9 +268,11 @@ let report_name_collision (id_to_string : id -> string)
\"" ^ name ^ "\":" ^ id1 ^ id2
^ "\nYou may want to rename some of your definitions, or report an issue."
in
- (* If we fail hard on errors, raise an exception - we don't link this error
- to any meta information because we already put the span information about
- the two problematic definitions in the error message above. *)
+ (* Register the error.
+
+ We don't link this error to any meta information because we already put
+ the span information about the two problematic definitions in the error
+ message above. *)
save_error __FILE__ __LINE__ None err
let names_map_get_id_from_name (name : string) (nm : names_map) :