From 944e0b34a1af6ee899b26a9469ffdc44b37f94d7 Mon Sep 17 00:00:00 2001 From: grunweg Date: Sat, 7 Sep 2024 13:01:51 +0000 Subject: [PATCH] chore: remove scripts/fix-by-linebreaks.sh (#16563) This script is currently unused; it was created during and for the port, and its functionality is incorporated into lint-style.py. --- scripts/fix-by-linebreaks.sh | 5 ----- 1 file changed, 5 deletions(-) delete mode 100755 scripts/fix-by-linebreaks.sh diff --git a/scripts/fix-by-linebreaks.sh b/scripts/fix-by-linebreaks.sh deleted file mode 100755 index f0fdd8aa12f08..0000000000000 --- a/scripts/fix-by-linebreaks.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/usr/bin/env bash -# Modify all lean files in mathlib to put the "by" in lines that only contain " by" at the end of the previous line, -# when the previous line with " by" appended is not longer than 100 characters. - -grep -lr "^ by\$" Mathlib | xargs -n 1 awk -i inplace '{do {{if (match($0, "^ by$") && length(p) < 98 && (!(match(p, "^[ \t]*--.*$")))) {p=p " by";} else {if (NR!=1) {print p}; p=$0}}} while (getline == 1) if (getline==0) print p}'