diff --git a/dev/make-distrib.sh b/dev/make-distrib.sh
index 391182f63a06991a2a58f9f997feb2c0049fc025..3b2b12e9932ee5ee82d9d3c4a5e2a347f9afcf0d 100755
--- a/dev/make-distrib.sh
+++ b/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/"