diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-22 09:06:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-06-22 09:06:58 +0200 |
| commit | b89904c3831f1ddc02efb2998c71dcaa0df1d286 (patch) | |
| tree | d31b761cb8cb722b14931ef83c1ca0d083a9f4db /dev | |
| parent | 37e8149db7bfa2e7d7fe571b92752f6589101852 (diff) | |
Fix Windows install script following removal of INSTALL.ide and move of INSTALL.doc.
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 } |