diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-03 15:55:00 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-10 10:31:21 +0200 |
| commit | 7ed370257e576dd084f89eae52fcc2135d4fbee3 (patch) | |
| tree | 7cac2dd8ba7fa918ac2e0eb9cdd1d0edcaf59afa /pretyping/recordops.mli | |
| parent | ab5d23b0a82fba784080946f6bb00dd123f64080 (diff) | |
Fix a oversight in 5bf9e67b .
About 8 months after making this commit, I realised that I forgot to change a tclORELSE into a tclOR (which was the whole point of the commit to begin with). Shame on me.
It does not seem to have much of an effect on efficiency, though. It may be a hair faster, but mostly indistinguishably so.
Diffstat (limited to 'pretyping/recordops.mli')
0 files changed, 0 insertions, 0 deletions