From aa0824da7ba08d7a30704e92e564c973fd10c555 Mon Sep 17 00:00:00 2001 From: Ed Page Date: Wed, 11 Mar 2026 07:38:23 -0500 Subject: [PATCH] chore(ci): Detect user changes to src/etc/man --- ci/validate-man.sh | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/ci/validate-man.sh b/ci/validate-man.sh index a3f114214dd..0ca822bd61a 100755 --- a/ci/validate-man.sh +++ b/ci/validate-man.sh @@ -5,8 +5,9 @@ set -e cargo_man="src/doc" mdman_man="crates/mdman/doc" +man_out="src/etc/man" -changes=$(git status --porcelain -- $cargo_man $mdman_man) +changes=$(git status --porcelain -- $cargo_man $mdman_man $man_out) if [ -n "$changes" ] then echo "git directory must be clean before running this script." @@ -15,7 +16,7 @@ fi cargo build-man -changes=$(git status --porcelain -- $cargo_man $mdman_man) +changes=$(git status --porcelain -- $cargo_man $mdman_man $man_out) if [ -n "$changes" ] then echo "Detected changes of man pages:"