diff options
author | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-31 15:51:15 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:36:05 +0200 |
commit | 7fe9c86423ee46f8283233dab555084abd138ce9 (patch) | |
tree | 42efc48c12ae5ab2da32c10bf6a62082cf0c4edf /parsing/g_prim.mlg | |
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 'parsing/g_prim.mlg')
0 files changed, 0 insertions, 0 deletions