aboutsummaryrefslogtreecommitdiffhomepage
path: root/.circleci
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-10 15:23:45 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-05-11 15:55:59 +0200
commitf20a053364421c6f5691bb02c9015a9db5cbfafe (patch)
tree3d8dbbdff6629521ff4d02eb562e1ab9015d0aa0 /.circleci
parent0acaa906367c02c57a6d70dd5d19eaea884b7568 (diff)
Notations: advertize that distinct "only parsing"/"only printing" rules work.
Diffstat (limited to '.circleci')
0 files changed, 0 insertions, 0 deletions