aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-11-05 14:09:54 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 09:35:15 +0100
commitcd60731dae4e7627588027fe1c1aa60a2ae44594 (patch)
treeea34807535fb5d20536c59a45f4c616dde5eb3cb /plugins/omega
parent3600dbb0546a910cda3996b5226bd7a6800d3040 (diff)
FIX: removing references to Γ which is not defined in a given context
Diffstat (limited to 'plugins/omega')
0 files changed, 0 insertions, 0 deletions