aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-05-09 10:03:37 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-06-13 10:32:32 +0200
commit22ca6b0d70bb8b49aaa420f844c75592e5781c21 (patch)
tree865c0332b3a52a1af6ae9ebc26a2e5eb07518de6 /plugins/omega
parent6332f43dfee3efc890c5f8fdc1b5b54942c16307 (diff)
Turn the default behaviour of the refine primitive into the safe one.
Diffstat (limited to 'plugins/omega')
0 files changed, 0 insertions, 0 deletions