From f58161f23ccb4bff2080a7c63105d80777c33362 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 4 Apr 2024 11:00:23 +0200
Subject: Update a comment

---
 compiler/ExtractBase.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'compiler')

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) :
-- 
cgit v1.2.3