diff options
| author | Gaëtan Gilbert | 2017-08-31 15:51:15 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-03 13:36:05 +0200 |
| commit | 7fe9c86423ee46f8283233dab555084abd138ce9 (patch) | |
| tree | 42efc48c12ae5ab2da32c10bf6a62082cf0c4edf /kernel/nativecode.ml | |
| parent | c17b3248f3473ec464ab19196558533f621d796c (diff) | |
Modops.add_retroknowledge: remove unused argument.
Unused since fe1979bf47951352ce32a6709cb5138fd26f311d.
I'm not sure if it was actually used back then since I didn't look at
the function it was passed to.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions