summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorDavid Allsopp <david.allsopp@metastack.com>2022-04-19 19:42:07 +0100
committerDavid Allsopp <david.allsopp@metastack.com>2022-07-22 08:15:51 +0100
commit055023e6a4f0b798e11573ccb85e0c17782a922a (patch)
tree231ed55ae0ff512afdc04ca6685e850d3bdfc954 /tools
parent6f7fff7330698be963f72004b85382e3bee3e2c2 (diff)
downloadocaml-055023e6a4f0b798e11573ccb85e0c17782a922a.tar.gz
Log the result of "Check for manual changes"
Especially now that it's in a separate build stage.
Diffstat (limited to 'tools')
-rwxr-xr-xtools/ci/actions/check-manual-modified.sh1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/ci/actions/check-manual-modified.sh b/tools/ci/actions/check-manual-modified.sh
index 782b5dee47..57cdbe50d6 100755
--- a/tools/ci/actions/check-manual-modified.sh
+++ b/tools/ci/actions/check-manual-modified.sh
@@ -31,4 +31,5 @@ else
fi
fi
+echo "Manual altered: $result"
echo "::set-output name=changed::$result"