diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-10-10 03:45:03 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-10-10 03:49:50 -0400 |
| commit | 5b0769b33004202d015770aff3f3cdd347b099fb (patch) | |
| tree | e3964c2163d73fbda3fd57be683f6e1c821e23e4 /kernel/retroknowledge.ml | |
| parent | ba50753e9da60a23a40dedea59fb7f25e3ba4d15 (diff) | |
Fix segfault in native compiler on int31 division.
Thanks to Yves for reporting it!
Diffstat (limited to 'kernel/retroknowledge.ml')
| -rw-r--r-- | kernel/retroknowledge.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index b645e256f..8b451e2b8 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -57,6 +57,7 @@ type int31_field = | Int31TimesC | Int31Div21 | Int31Div + | Int31Diveucl | Int31AddMulDiv | Int31Compare | Int31Head0 |