diff options
Diffstat (limited to '.github/workflows/compare-manuals.sh')
-rwxr-xr-x | .github/workflows/compare-manuals.sh | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/.github/workflows/compare-manuals.sh b/.github/workflows/compare-manuals.sh deleted file mode 100755 index b2cc68c7831..00000000000 --- a/.github/workflows/compare-manuals.sh +++ /dev/null @@ -1,21 +0,0 @@ -#!/usr/bin/env nix-shell -#! nix-shell -i bash -p html-tidy - -set -euo pipefail -shopt -s inherit_errexit - -normalize() { - tidy \ - --anchor-as-name no \ - --coerce-endtags no \ - --escape-scripts no \ - --fix-backslash no \ - --fix-style-tags no \ - --fix-uri no \ - --indent yes \ - --wrap 0 \ - < "$1" \ - 2> /dev/null -} - -diff -U3 <(normalize "$1") <(normalize "$2") |