# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1739558067 -3600
# Node ID 0dd633d9ae63b2170b35d718872569c263b9b5fd
# Parent  3f3769c50bf5d9ab5c8ca806ce89efff8521613f
proper synonyms: special characters need to be escaped;

diff -r 3f3769c50bf5 -r 0dd633d9ae63 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Fri Feb 14 18:06:51 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Fri Feb 14 19:34:27 2025 +0100
@@ -142,7 +142,9 @@
         if !Special_Char.matches(symbol) && !Arrow.matches(symbol)
       } yield symbol + " => " + code
 
-    override lazy val more_config = Map(Path.basic("synonyms.txt") -> synonyms.mkString("\n"))
+    override lazy val more_config =
+      Map(Path.basic("synonyms.txt") ->
+        Solr.escape(synonyms.mkString("\n"), Solr.special -- Solr.wildcard_char.map(_.toString)))
 
     object Types {
       private val strip_html = Solr.Class("charFilter", "HTMLStripCharFilterFactory")