diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-26 14:52:51 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-26 14:52:51 +0200 |
| commit | 7c28b7fa4816dab697f60b397884021ddc081ba2 (patch) | |
| tree | 5789665bb704d43985b7b96c41badae4e688bb01 /dev | |
| parent | fb9c581491715c4c34054a744426318a6991c9ed (diff) | |
| parent | b89904c3831f1ddc02efb2998c71dcaa0df1d286 (diff) | |
Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 508dcf5fb..a59afb8f6 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1128,14 +1128,12 @@ function copy_coq_license { install -D doc/LICENSE "$PREFIXCOQ/license_readme/coq/LicenseDoc.txt" install -D LICENSE "$PREFIXCOQ/license_readme/coq/License.txt" install -D plugins/micromega/LICENSE.sos "$PREFIXCOQ/license_readme/coq/LicenseMicromega.txt" - install -D README "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true - install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true - install -D README.win "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true - install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true + # 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 "$PREFIXCOQ/license_readme/coq/Changes.txt" install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" - install -D INSTALL.doc "$PREFIXCOQ/license_readme/coq/InstallDoc.txt" - install -D INSTALL.ide "$PREFIXCOQ/license_readme/coq/InstallIde.txt" + install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" fi } |