# HG changeset patch
# User wenzelm
# Date 1646220526 -3600
# Node ID 7d1864ffad13b66c8432c121a666863d281a5b96
# Parent  26ac98871d4201010a510a17489d2c8f5144fd85
more robust;

diff -r 26ac98871d42 -r 7d1864ffad13 src/Tools/VSCode/extension/src/library.ts
--- a/src/Tools/VSCode/extension/src/library.ts	Mon Feb 28 14:53:52 2022 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts	Wed Mar 02 12:28:46 2022 +0100
@@ -8,7 +8,7 @@
 
 export function escape_regex(s: string): string
 {
-  return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&")
+  return s.replace(/[|\\{}()[\]^$+*?.]/g, "\\$&").replace(/-/g, '\\x2d')
 }
 
 /* strings */