tuned;

--- a/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 15:04:59 2022 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 15:06:09 2022 +0100
@@ -10,9 +10,10 @@
 
 export function escape_regex(s: string): string
 {
-  return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&").replace(/-/g, '\\x2d')
+  return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&").replace(/-/g, "\\x2d")
 }
 
+
 /* strings */
 
 export function quote(s: string): string