summaryrefslogtreecommitdiff
path: root/dune-project
diff options
context:
space:
mode:
authorSon Ho2022-01-28 21:34:55 +0100
committerSon Ho2022-01-28 21:34:55 +0100
commit0b145dd4b0ab0ac5ed56121663a25801f20bed67 (patch)
treea865bf9689d1485c7ed195cc4f181a85cd3bf686 /dune-project
parent21dddf2fc6c09495de56250961ab69b2b6506112 (diff)
Make minor modifications
Diffstat (limited to 'dune-project')
0 files changed, 0 insertions, 0 deletions