From eae7ce912c8bae44f98e1d489aba5618c0029bd2 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 10:59:46 +0200 Subject: Make a minor modification --- compiler/ExtractBase.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 451c2c41..d760ab1e 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -268,8 +268,10 @@ 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 *) - save_error __FILE__ __LINE__ meta1 err + (* 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. *) + save_error __FILE__ __LINE__ None err let names_map_get_id_from_name (name : string) (nm : names_map) : (id * Meta.meta option) option = -- cgit v1.2.3