diff --git a/dev/make-distrib.sh b/dev/make-distrib.sh
index 18733a1b3b7c8c73f0b528714c4042bee2bb1e75..2000ad90ec86bf4c0753ee2ea0d6295e41da03d0 100755
--- a/dev/make-distrib.sh
+++ b/dev/make-distrib.sh
@@ -60,6 +60,16 @@ if [ "$VERSION" != "$OPAM_VERSION" ]; then
   exit 2
 fi
 
+################################################################################
+# Check that no versioned file is ignored
+
+IGNORED_FILES="$(git ls-files --ignored --exclude-standard -c)"
+if [ "" != "$IGNORED_FILES" ]; then
+  echo "Some versioned files are ignored by .gitignore:"
+  echo $IGNORED_FILES
+  exit 2
+fi
+
 ################################################################################
 # Prepare archive