diff options
| author | Théo Zimmermann | 2018-11-20 19:48:13 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-11-20 19:48:13 +0100 |
| commit | 4449c990dee9980bb748988aa053f5462914cb3c (patch) | |
| tree | cc0337eeaa211bb774a0d07a20173b2b5a63ffba /kernel | |
| parent | fc9c25270f22e2e34c45d47f0362d543c1bd2421 (diff) | |
| parent | f858025ac2e980b8b00fc8428c8b59ae3d27a1c4 (diff) | |
Merge PR #9035: [dune] Only build printers when the ltac plugin is available.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions