diff options
| author | Arnaud Spiwack | 2014-10-16 10:21:17 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-16 10:37:53 +0200 |
| commit | 025c4f63b28671a24bd6c46f9b23a3dad76fd179 (patch) | |
| tree | 2759d9c0eaa5e62329727677bf54caf06ac9ffe6 /kernel/nativecode.ml | |
| parent | e6708590ce648921f27395ce535e35d52aa2cc0f (diff) | |
Goal: remove [advance] from the API.
Now [Goal] only contains a few helpers.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions