aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/votour.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-21 18:19:46 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-26 14:53:08 +0100
commitf1e1452841997c08217bd4caf1da8370f17c93f3 (patch)
tree457833423fdc28e0af5252cfc87a59ee4bb31af9 /checker/votour.ml
parent23a33c1a7781e35faf83ed4c7e42df8c8803e64e (diff)
checker: less useless error messages
Diffstat (limited to 'checker/votour.ml')
0 files changed, 0 insertions, 0 deletions