aboutsummaryrefslogtreecommitdiffhomepage
path: root/.travis.yml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-06 17:36:18 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-08 01:10:55 +0200
commit818ba539cf4a0aed2172f370dcddd380b6ec6a4c (patch)
tree4eddde38a39038139f4771adbcb0c8db8cf5d148 /.travis.yml
parent0b6f9dafdd828466ab87306f30f3aae0bc689f4f (diff)
[CoqProject] Add some comments and remove unnecessary use of Pp.
But indeed we need to split this file, as it is used now from CoqIDE is incorrect.
Diffstat (limited to '.travis.yml')
0 files changed, 0 insertions, 0 deletions