diff options
| author | Emilio Jesus Gallego Arias | 2019-01-22 14:28:46 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-22 14:28:46 +0100 |
| commit | d88f9883ce8313c82cb081987e30de1d7201805e (patch) | |
| tree | 872d1012eb3d6e5cbed124bcf60b3604429abe70 /dev/ci/ci-wrapper.sh | |
| parent | 4cfe350210f2390f90c49262c1c8a2c64f626c3e (diff) | |
| parent | 229a876f63b17fa9d472f7e972a3004fa1e50294 (diff) | |
Merge PR #9308: Remove outdated gitignore coqprojectfile.ml
Reviewed-by: ejgallego
Diffstat (limited to 'dev/ci/ci-wrapper.sh')
0 files changed, 0 insertions, 0 deletions