diff options
| author | Théo Zimmermann | 2017-11-15 17:50:51 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-12-08 16:51:10 +0100 |
| commit | 3c2b1b7f99a1e06ad86a3c5dbf8369d773928e85 (patch) | |
| tree | 0bd8648bd40e3f881107a5e5f1d210e4289499ae /dev | |
| parent | 2bd31e5fffbd6722f20016c3962088ab2008e2c0 (diff) | |
Adapt to removal of match_appsubterm.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions