aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-17 18:53:45 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-17 19:10:55 +0100
commit8a179389fe5199e79d05b2c72ff2aae2061820aa (patch)
tree5ffaca3f0ab4faaf8b21f8ca05b6e20def9f9c91 /configure
parent65b901534649c5f29e245a4960fa66f6e9d9c257 (diff)
Fixing the Proofview.Goal.goal function.
The environment put in the goals was not the right one and could lead to various leaks.
Diffstat (limited to 'configure')
0 files changed, 0 insertions, 0 deletions