diff options
| author | Hugo Herbelin | 2018-09-28 18:40:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-28 18:51:02 +0200 |
| commit | 2ea68be1bf7b5977234957f8ad04fdaa0ce539a2 (patch) | |
| tree | e798ed949c909b949ae04b4fc29e59653a119077 /kernel/nativelib.ml | |
| parent | 0bcbc990dcebce2e66f10aba462c9fed2c2eda06 (diff) | |
Functionalizing calls to the environment in Himsg.
This shall eventually allow to call Himsg at any point of the
execution, independently of the exact current global environment.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions