aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-07 01:31:24 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-07 01:31:24 +0100
commit168f7a6415ad86a015c1f793b97554cb1d9e45bc (patch)
tree6bd420952e8e08e02bfbcd8a7db0c0ef0bb8955c /printing
parent480082fe4a15dbd5d8ed2e9820a6329db10442bf (diff)
parentdddfbd00053a761581ea496fdddad2bc5bc14ec8 (diff)
Merge PR#436: [ocamlbuild] Update META for the vernac split.
Diffstat (limited to 'printing')
0 files changed, 0 insertions, 0 deletions