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 /.gitignore | |
| parent | 4cfe350210f2390f90c49262c1c8a2c64f626c3e (diff) | |
| parent | 229a876f63b17fa9d472f7e972a3004fa1e50294 (diff) | |
Merge PR #9308: Remove outdated gitignore coqprojectfile.ml
Reviewed-by: ejgallego
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index dfecfec837..2e5529ccfb 100644 --- a/.gitignore +++ b/.gitignore @@ -134,7 +134,6 @@ coqpp/coqpp_parse.mli g_*.ml -lib/coqProject_file.ml plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml plugins/ltac/extraargs.ml |