| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Normalization sounds like it should be semantically noop.
|
|
|
|
|
|
|
|
`apply.whitespace = fix`
|
|
|
|
Having `--whitespace=` on all `git apply` in this script should make it
insensitive to user setup in `~/.gitconfig`, at least
`[apply] whitespace = fix`.
Note that even this way, this script remains hugely fragile and non mature,
and would better *not* be set by default for everybody.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Like circle CI we install every opam package in opam-boot jobs (one
per switch).
This should be more reliable with less issues from outdated cache.
Also avoid messing with symlinks through OPAMROOT (we can't
cache/artifact files outside the coq directory).
Avoid using "system" compiler (no risk of getting an upgrade through
the base image).
|
|
|
|
- BUILD_TARGET not used
- Put elpi's FINDLIB_VER="" at the end of the environment for nicer
display in the travis UI.
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #6963.
|
|
|
|
|
|
|
|
|
|
|
|
This changed in https://github.com/coq/coq/commit/35961a4ff5a5b8c9b9786cbab0abd279263eb655
|
|
|
|
|
|
|
|
|
|
|
|
Most of these warnings should really be errors (ill-formed input,
invalid cross references, etc.) so we make it the default.
|
|
|
|
The Ubuntu Font License requires substantially modified fonts to be renamed
entirely.
|
