diff options
| author | Robert Norton | 2018-07-05 16:17:01 +0100 |
|---|---|---|
| committer | Robert Norton | 2018-07-05 17:14:31 +0100 |
| commit | 86194c561fbb9ea24b28f413f16211d5920bb362 (patch) | |
| tree | 056226ef72c53dab7a15d1edbdeb035493b3a7d4 /lib/hol | |
| parent | 35ecc1210857dc9e3791483910be4c6e47325b76 (diff) | |
make many generated c functions static -- this gives the compiler a chance to notice if they are dead or inline them if appropriate, cleaning up coverage reports and potentially improving execution speed.
Diffstat (limited to 'lib/hol')
0 files changed, 0 insertions, 0 deletions