diff options
| author | Jasper Hugunin | 2020-09-09 10:23:51 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | ecb29318d6b818b758ecf6d4a06dbde8838e7a04 (patch) | |
| tree | d0695129b20f21d2d1c4b00149fa9a6c7db5e45a /doc/plugin_tutorial/tuto1 | |
| parent | c66266493b3678814604365386e4b7afc362483c (diff) | |
Modify Numbers/Natural/Abstract/NAdd.v to compile with -mangle-names
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions