aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.checker
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-19 15:43:39 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-10-19 17:05:39 +0200
commit21e1d501e17c9989d9cd689988a510e1864f817a (patch)
tree2bb19e8fe38ad80c2cb3266eaba47aa85d9906c7 /Makefile.checker
parent6fbe3c850bac9cbdfa64dbdcca7bd60dc7862190 (diff)
Attempt to improve error rendering in pattern-matching compilation (#5142).
When trying different possible return predicates, returns the error given by the first try, assuming this is the most interesting one.
Diffstat (limited to 'Makefile.checker')
0 files changed, 0 insertions, 0 deletions