aboutsummaryrefslogtreecommitdiff
path: root/dev/build
diff options
context:
space:
mode:
authorThéo Zimmermann2019-04-16 18:27:14 +0200
committerThéo Zimmermann2019-05-05 19:22:32 +0200
commit30d6ffdd4546d56c517bef5b31a862c5454240f0 (patch)
tree7fe923020598b54da28ad0043ef12481d1e300e8 /dev/build
parent6ff10c569c1684927d4cb866a159fe6f54e55abe (diff)
New infrastructure for the unreleased changelog.
Move existing entries.
Diffstat (limited to 'dev/build')
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh1
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 4c5bd29236..ea9af60330 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1316,7 +1316,6 @@ function copy_coq_license {
# FIXME: this is not the micromega license
# It only applies to code that was copied into one single file!
install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md"
- install -D CHANGES.md "$PREFIXCOQ/license_readme/coq/Changes.md"
install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt"
install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
fi