summaryrefslogtreecommitdiff
path: root/src/Makefile
diff options
context:
space:
mode:
authorRobert Norton2017-04-21 17:03:23 +0100
committerRobert Norton2017-04-21 17:05:28 +0100
commita5d8b2dc56594c1c4d1f88b1017638b5eef69086 (patch)
tree55337a03b43ad3323d6aeda617fb217f1688de3a /src/Makefile
parente55f01ec8a3b3e94818d1701e28d1e9fa6343166 (diff)
define some big_int literals in sail_values.ml to avoid lots of calls to bit_int_of_int. Likely very little performance benefit but slightly more readable.
Diffstat (limited to 'src/Makefile')
0 files changed, 0 insertions, 0 deletions