aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-31 14:18:50 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-31 14:18:50 +0200
commit13fb8de9aff07e4346ca4bdc866507503e9be12e (patch)
tree3ba390e7b32d0909a92d964a27c94eb9da3214c2 /Makefile.doc
parentbed414f560e3db511ca3a647acce6e5ebc70b4cc (diff)
parent86dbe3337197741d0ceaea740cbbd3e8b9b1dfe1 (diff)
Merge PR #992: Fix BZ#5687: Coqtop died badly modal message box from CoqIDE.
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions