diff options
| author | Jasper Hugunin | 2020-09-09 10:44:43 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | 13a9a7f16acb520b1e38aeac9480f7d298a62bc7 (patch) | |
| tree | db02930772c41cb56226cbe5ee3ccebfe246df98 /doc/plugin_tutorial/tuto2 | |
| parent | 2128f623d1d9f26b5791d65e95c8d624ac7e48b9 (diff) | |
Modify Numbers/Natural/Abstract/NGcd.v to compile with -mangle-names
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions