[distrib] check ignored files before distrib

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