# HG changeset patch
# User wenzelm
# Date 1646229969 -3600
# Node ID e3388efdacd7d9b0aabaef9820e6d8b1e39c8b6b
# Parent  5651855f570ee968aa450170ee28e5194a31b7de
tuned;

diff -r 5651855f570e -r e3388efdacd7 src/Tools/VSCode/extension/src/library.ts
--- 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