aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/libnames.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-27 17:26:22 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-27 17:26:22 +0100
commit437f20f0a1c2717cd7baae52e2ab20750dd9d4fb (patch)
tree5586b6b33fbe7ccaff33dd9fab4edefd30cb98a4 /library/libnames.ml
parentc5ccbf0f4cb4d0dbfbc94cb71f3bdfe1ca888698 (diff)
parent4a9295baa83c1922d9defd601ed410d0a8241135 (diff)
Merge PR #6237: coq_makefile tests: build in easily removed temporary subdirectory.
Diffstat (limited to 'library/libnames.ml')
0 files changed, 0 insertions, 0 deletions