diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-26 16:37:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-27 00:28:50 +0200 |
| commit | 05bd0ab1dd85764874ca077005dcaff5414589a5 (patch) | |
| tree | 40ecae5fc60a644761898bcb61e13ef463efecb6 /tools | |
| parent | b818c00e3e895ea9b736ab968e3ba109b0fd67c1 (diff) | |
Moving setting of "cleared" evar flag directly in Evd.restrict.
In particular, this fixes #5757 which used restrict_evar to refine the
information on the source of an evar, and which should have set the
"cleared" flag.
Also renaming flag "restricted" since it is not only about "clear".
I guess this is what we want in general, but I did not survey all uses
of restrict_evar so, maybe, this should be refined further.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions