# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1739574776 -3600
# Node ID a3d94cf1457a72e47966ba9f545b2c30d5261e2b
# Parent  a984f543ed924450384ce37c6a78cf22747e456e
properly handle whitespace characters: must be escaped individually;

diff -r a984f543ed92 -r a3d94cf1457a src/Tools/Find_Facts/src/solr.scala
--- a/src/Tools/Find_Facts/src/solr.scala	Fri Feb 14 23:46:40 2025 +0100
+++ b/src/Tools/Find_Facts/src/solr.scala	Sat Feb 15 00:12:56 2025 +0100
@@ -54,7 +54,7 @@
   def term(b: Boolean): Source = b.toString
   def term(i: Int): Source = i.toString
   def term(s: String): Source =
-    "(\\s+)".r.replaceAllIn(escape(s, special), ws => "\\\\" + ws.matched)
+    "(\\s)".r.replaceAllIn(escape(s, special), ws => "\\\\" + ws.matched)
 
   def range(from: Int, to: Int): Source = "[" + from + " TO " + to + "]"
   def phrase(s: String): Source = quote(escape(s, special))