Merge remote-tracking branch 'phymbert/master' into hp/server/deps-check-TEST-dirty

# Conflicts:
#	.github/workflows/server.yml

Author: phymbert

.github/workflows/server.yml

@@ -74,8 +74,8 @@ jobs:
           git status
           ./deps.sh
           git status
-          git ls-files --others --modified
           not_ignored_files="$(git ls-files --others --modified)"
+          echo "Modified files: ${not_ignored_files}"
           if [ -n "${not_ignored_files}" ]; then
             echo "Repository is dirty or server deps are not built as expected"
             echo "${not_ignored_files}"