diff options
| author | Jason Gross <jasongross9@gmail.com> | 2020-04-07 08:53:51 -0400 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-07 09:53:51 -0300 |
| commit | 994f99fc353f523dfe5633067805a1dd4a53040f (patch) | |
| tree | b79823dcc43a47e04dac948ce3866af32f1626fb | |
| parent | 2f75277037d172200d4a37621c1b9c3b9901dbd8 (diff) | |
| download | gitignore-994f99fc353f523dfe5633067805a1dd4a53040f.tar.gz gitignore-994f99fc353f523dfe5633067805a1dd4a53040f.zip | |
Add generated timing files to Coq.gitignore (#3367)
These generated files were added in https://github.com/coq/coq/pull/745
| -rw-r--r-- | Coq.gitignore | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Coq.gitignore b/Coq.gitignore index a3e2ac49..829ac44a 100644 --- a/Coq.gitignore +++ b/Coq.gitignore @@ -31,3 +31,13 @@ lia.cache nia.cache nlia.cache nra.cache + +# generated timing files +*.timing.diff +*.v.after-timing +*.v.before-timing +*.v.timing +time-of-build-after.log +time-of-build-before.log +time-of-build-both.log +time-of-build-pretty.log |