diff --git a/src/lake/Lake/Util/Newline.lean b/src/lake/Lake/Util/Newline.lean new file mode 100644 index 000000000000..54a0272dbc98 --- /dev/null +++ b/src/lake/Lake/Util/Newline.lean @@ -0,0 +1,10 @@ +/- +Copyright (c) 2023 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro +-/ + +namespace Lake + +/-- This is the same as `String.replace text "\r\n" "\n"`, but more efficient. -/ +@[inline, deprecated] partial def crlf2lf (text : String) : String := text.crlfToLf