diff options
| author | Maxime Dénès | 2018-09-26 16:20:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 16:20:07 +0200 |
| commit | 118a93ccf954d02afbfa5ef2b3735ef37439b274 (patch) | |
| tree | cf9d5ba237d1fcdf18aaca6b2d880a6cd96e365f /doc/plugin_tutorial/tuto1/src/dune | |
| parent | ccb701d78394a108daf25e62d40ba059aa3fce62 (diff) | |
Adapt to removal of section paths from kernel names
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/dune')
0 files changed, 0 insertions, 0 deletions