aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-10 21:54:21 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-10 21:56:06 +0100
commit525c0e434e9b9472b6249bfd575659eb2dbec206 (patch)
tree1e72d9ee4c7cf094507207555c625927709255ad /Makefile.doc
parentf804e681f1550e1c20b8ce5b83bc66c876fb3c99 (diff)
Fixing #4001 (missing type constraints when building return clause of match).
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions