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 /dev/base_include | |
| parent | acefe58cd39c9a4efee632f7f92f56fb4d5285bb (diff) | |
Extract section on records from Gallina extensions.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions