aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-01-22 10:10:39 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-05-23 10:48:27 +0200
commitcd8f10fe54c956f1e797da3d165c3b29ffee615b (patch)
tree5d0013edae593e0f9fb507e22b73ee411ec0e7ee /test-suite/coq-makefile
parentbf84180f963a31d1ec850d4ccedd599f2984ea9b (diff)
configure: -local set coqdoc destination dir to ./doc rather than ""
Diffstat (limited to 'test-suite/coq-makefile')
0 files changed, 0 insertions, 0 deletions