From 10607bd9eda70c9b41de93177e9fb98bf4796c8c Mon Sep 17 00:00:00 2001 From: Kilian Ciuffolo Date: Wed, 15 May 2024 12:29:06 -0700 Subject: [PATCH] .. --- scripts/push.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/push.sh b/scripts/push.sh index 3d29d82..c2ee62e 100755 --- a/scripts/push.sh +++ b/scripts/push.sh @@ -29,8 +29,8 @@ cd "${cover_dir}" # beautify html for file in "revisions/${REVISION}.html" "revisions/${REVISION}-inc.html"; do - ex -sc '%s/