diff options
| author | Théo Zimmermann | 2017-06-22 16:33:13 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-06-22 16:34:09 +0200 |
| commit | cdd6e87e0a8df4b6af4a08353f260fb035af48fb (patch) | |
| tree | 051d662134dff2b33f3a4d8ace31387651e511ee /stm/asyncTaskQueue.mli | |
| parent | d30ed5fe0694466f70eed51bc689cd0fa8c00da5 (diff) | |
Ignore all PDF files.
Rules for ignoring *some* PDF files had been added one by one to `.gitignore`
but some were still missing (for the corresponding latex files in `dev`).
This rule is actually better since we are not tracking any PDF file.
Diffstat (limited to 'stm/asyncTaskQueue.mli')
0 files changed, 0 insertions, 0 deletions