Merge branch 'feature/andre/dev-make-distrib-warn' into 'master'

[dev] make-distrib.sh: warn about uncommitted changes

See merge request frama-c/frama-c!3997

dev/make-distrib.sh

@@ -71,6 +71,18 @@ if [ "" != "$IGNORED_FILES" ]; then
 fi
 
 ################################################################################
+
+################################################################################
+# Warn if there are uncommitted changes (will not be taken into account)
+
+GIT_STATUS="$(git status --porcelain)"
+if [ "" != "$GIT_STATUS" ]; then
+    echo "WARNING: uncommitted changes will be IGNORED when making archive:"
+    echo "$GIT_STATUS"
+fi
+
+################################################################################
+
 # Prepare archive
 
 git archive HEAD -o $FRAMAC_TAR --prefix "$FRAMAC/"