aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-07-02 20:03:03 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-07-02 20:03:03 +0200
commit1d6b4a6728066d0e684a4f996b6077018b79a620 (patch)
tree58474eb943b498255f37edd5cbd73ec116c556ce /dev
parenta4306c357407c8d5e10eb35bb270f4bde5287c78 (diff)
Rename the "chan" argument into "fmt" in coqpp_main.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions