diff options
| author | Emilio Jesus Gallego Arias | 2018-11-06 11:33:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 06:37:05 +0100 |
| commit | 4e9bc09df64cd15e85c19ecabbc9580c00771176 (patch) | |
| tree | d5a9c68561a5d7573641053580b95bc3c7c9be43 /dev/tools/github-check-prs.py | |
| parent | f8a76b3d383abf468fb21df509f5da8f8aafa913 (diff) | |
[CoqProject] Abstract warning function for CoqProject readers.
`CoqProject_file` uses the feedback system, however this is not very
convenient in some scenarios such as `coqdep` that has to be run very
early in the build process [and thus in "boot" mode].
We thus make the warning function a paramater.
Should fix #8913.
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions