diff options
| author | Pierre-Marie Pédrot | 2015-10-19 22:52:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-20 13:04:00 +0200 |
| commit | f5d8d305c34f9bab21436c765aeeb56a65005dfe (patch) | |
| tree | 7271ad90ee24db93003af945bdaea73ef1aa6787 /kernel/nativecode.mli | |
| parent | a104cd04f3d245bb45e6ff1db8b4ac10c51f4123 (diff) | |
Renaming Goal.enter field into s_enter.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions