diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-14 00:17:06 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-14 00:17:06 +0100 |
| commit | bbae426407ba7df585c22ec687a79c0cf216a6a8 (patch) | |
| tree | 3005a61d1997d772a9bb8be5389408f933d46033 /kernel/declareops.mli | |
| parent | ecacc9af6100f76e95acc24e777026bfc9c4d921 (diff) | |
[library] Don't recompute path_prefix on unfreeze.
We instead save the current value.
Diffstat (limited to 'kernel/declareops.mli')
0 files changed, 0 insertions, 0 deletions