summaryrefslogtreecommitdiff
path: root/dune-project
diff options
context:
space:
mode:
authorSon Ho2021-11-18 14:56:34 +0100
committerSon Ho2021-11-18 14:56:34 +0100
commit5ff58d77f3aa64d05108919326bbd9d3a5e99bac (patch)
tree7c83c47764f1dbcc5658bfb635b40dd780df7118 /dune-project
parent7491a243038de5d6256c40d3587b304c1f4895e8 (diff)
Cleanup a bit
Diffstat (limited to 'dune-project')
0 files changed, 0 insertions, 0 deletions