aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/future.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2013-12-20 17:29:35 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-01-04 17:07:15 +0100
commit0582c9363fa981798811ff11ef0e8c76c38255f7 (patch)
tree2ba490e8ad6424ea86ead50d0c91ba0f7ed0cd8d /lib/future.mli
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.mli')
0 files changed, 0 insertions, 0 deletions