diff options
| author | Théo Zimmermann | 2020-04-03 12:42:30 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-03 15:40:25 +0200 |
| commit | 3c8747bc2ea079cdca6c3b69f088bc536555863b (patch) | |
| tree | a78179057a64f455eb7e57606f1d6cabd9c5137e /doc/plugin_tutorial/tuto1 | |
| parent | acefe58cd39c9a4efee632f7f92f56fb4d5285bb (diff) | |
Extract section on records from Gallina extensions.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions