aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0
diff options
context:
space:
mode:
authorJasper Hugunin2020-08-25 13:14:04 -0700
committerJasper Hugunin2020-08-25 13:53:33 -0700
commit9cd62a46c1db28e3bc77711ee6e7ab8e887ce494 (patch)
tree50e13c709fce71c6b30b72dd0ca28d4848fbc59f /doc/plugin_tutorial/tuto0
parent1b6b14b1727a74a56727e38a1c58b1d93747135b (diff)
Modify Numbers/NatInt/NZMul.v to compile with -mangle-names
Diffstat (limited to 'doc/plugin_tutorial/tuto0')
0 files changed, 0 insertions, 0 deletions