Include CHANGES file in dist.

liffiton · Nov 11, 2014 · 45a706d · 45a706d
1 parent 3e74c97
commit 45a706d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/mkdist.sh b/mkdist.sh
@@ -1,7 +1,7 @@
 #!/bin/bash
 
 # gather "whitelist" of files to include
-marco_files="*.py muser2-static README VERSION"
+marco_files="*.py muser2-static README CHANGES* VERSION"
 if [ $# -lt 2 -o "$2" != "notest" ] ; then
     test_files="tests/*.cnf tests/*.gcnf tests/*.smt2 tests/*.gz tests/*.py tests/out/*/*"
 fi