diff options
| author | Columbus240 | 2020-08-24 19:27:33 +0200 |
|---|---|---|
| committer | Columbus240 | 2020-09-12 23:00:19 +0200 |
| commit | a8be1e2551bc4fbda9c45792c0dad5743c18fefd (patch) | |
| tree | 0fe098cb2dee92d3756b6ce01e721de0ea56e080 /lib | |
| parent | 8f5b97b4315440e75658ce2165761bf086ad3e11 (diff) | |
Merge some of the gitignore files
Both /.gitignore and /lib/coq/.gitignore ignored some files in /lib/coq.
This commit removes /lib/coq/.gitignore and moves all ignore-statements
to /.gitignore . This should simplify the maintenance of gitignore files.
The situation with /test/mono/.gitignore is analogous.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/.gitignore | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/coq/.gitignore b/lib/coq/.gitignore deleted file mode 100644 index 1aa62803..00000000 --- a/lib/coq/.gitignore +++ /dev/null @@ -1 +0,0 @@ -deps
\ No newline at end of file |