summaryrefslogtreecommitdiff
path: root/dune-project
diff options
context:
space:
mode:
authorSon Ho2022-02-03 23:22:02 +0100
committerSon Ho2022-02-03 23:22:02 +0100
commit1b8b473bb3325713b72e12c7adfba3e024fdf194 (patch)
tree9261f14ef4a8ab629f233f16f3aad562e2d0b36d /dune-project
parentf7f5d626745200df5748e7bda860c7d303bea18a (diff)
Make a minor improvement in printing
Diffstat (limited to 'dune-project')
0 files changed, 0 insertions, 0 deletions