aboutsummaryrefslogtreecommitdiff
path: root/lib/future.ml
diff options
context:
space:
mode:
authorEnrico Tassi2013-12-20 17:29:35 +0100
committerEnrico Tassi2014-01-04 17:07:15 +0100
commit0582c9363fa981798811ff11ef0e8c76c38255f7 (patch)
tree2ba490e8ad6424ea86ead50d0c91ba0f7ed0cd8d /lib/future.ml
parent9bb1b959071575074870ba2a11ca79cb52cb7e8b (diff)
kernel: save in aux the list of section variables used
This has nothing to do with the kernel itself, but it is the place where this piece of data is inferred.
Diffstat (limited to 'lib/future.ml')
0 files changed, 0 insertions, 0 deletions