diff options
| author | Emilio Jesus Gallego Arias | 2020-09-15 19:09:45 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-09-15 19:22:01 +0200 |
| commit | 0022a52b04187414db4dba7cd797a23813078d67 (patch) | |
| tree | be3df50e61345b215c6e4e216d51dc089ca8c9fc /dev/include_dune | |
| parent | d6b6e1d6ceadfe65ea398786361ff7737624deaf (diff) | |
[vernac] Don't allow attributes on print / check
Fixes #11661
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions