aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-20 01:17:42 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-20 01:17:42 +0200
commite081531f95f02f0d4cb557f9ee331719e0b1ddd7 (patch)
treed895ee983b0e3c5105af561ccf9aa8e0a90ea8bc
parent6e25e6571100d627ddd332bcfa6c0a1605bcda9d (diff)
parent2b00427c545be77805c6e954c2fa9c45682fec85 (diff)
Merge PR#649: Fix a typo
-rw-r--r--dev/build/windows/makecoq_mingw.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 52b158871..98e80c765 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1082,7 +1082,7 @@ function make_coq {
copq_coq_gtk
copy_coq_license
- # make clean seems to br broken for 8.5pl2
+ # make clean seems to be broken for 8.5pl2
# 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile
# 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)"
# make clean