aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-29 11:20:26 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-02-29 13:24:45 +0100
commit7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f (patch)
tree31301a44d27401d5fad006c9b400c9dd8f0d4d16 /ide
parentd0bc16d1a0626f4137797bbf0c91e972a0ff43ac (diff)
Moving the "clearbody" tactic to TACTIC EXTEND.
Diffstat (limited to 'ide')
0 files changed, 0 insertions, 0 deletions