summaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-07-05 12:53:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2009-07-05 12:53:14 +0200
commit581c27825b108d2a0ab9ee8e068bde947ede8ddd (patch)
treea4952ddb2151334c909f66988ca828c81457c54b /checker
parentd43a92cbe2dd9b90393698e98eb96104b14c04fa (diff)
Call coqchk without -silentdebian/8.2.pl1+dfsg-2
Diffstat (limited to 'checker')
0 files changed, 0 insertions, 0 deletions