diff options
| author | Théo Zimmermann | 2018-09-21 14:10:23 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-21 14:10:23 +0200 |
| commit | bceb3bc784d5ce196e06815bd91963607a35a62c (patch) | |
| tree | f4a18b7a40bddb054e373b3fbf287c77e246c9eb /Makefile.dune | |
| parent | 90ace7786901aa2f1253cf3887bf3e5221c5dae7 (diff) | |
| parent | a597bb33eb9b3c9d70422d72e89bcbda90896ddb (diff) | |
Merge PR #8455: Move tests in bugs/ to bugs/closed/.
Diffstat (limited to 'Makefile.dune')
0 files changed, 0 insertions, 0 deletions