# HG changeset patch
# User wenzelm
# Date 1762179538 -3600
# Node ID 26e0aafd26ea61b701d42937f6c6a1d486b118d8
# Parent  07d36671409f0ea7a8bd6bdf3a9d3882a27aee5f
unused (see also da1108a6d249);

diff -r 07d36671409f -r 26e0aafd26ea src/Tools/VSCode/extension/src/library.ts
--- a/src/Tools/VSCode/extension/src/library.ts	Mon Nov 03 15:18:23 2025 +0100
+++ b/src/Tools/VSCode/extension/src/library.ts	Mon Nov 03 15:18:58 2025 +0100
@@ -28,11 +28,6 @@
   return s.split("").reverse().join("")
 }
 
-export function has_newline(text: string)
-{
-  return text.includes("\n") || text.includes("\r")
-}
-
 
 /* settings environment */