diff options
| author | Hugo Herbelin | 2020-08-13 16:52:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-13 16:52:31 +0200 |
| commit | 2dbeadd72658eaa09cc9a683656aa27a4f140d50 (patch) | |
| tree | 21fce2ffc13c7f708040b36e58508f4960b59b91 /dev/include_dune | |
| parent | ab2a867759745d846a75efe21e7208f560ccd7a5 (diff) | |
| parent | 82caf82d9d2282b00771d38b8b607a134497b192 (diff) | |
Merge PR #12718: Do not rely on higher-order interfaces for patterns in dnets.
Reviewed-by: herbelin
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions