summaryrefslogtreecommitdiff
path: root/dune-project
diff options
context:
space:
mode:
authorSon Ho2021-12-07 17:51:47 +0100
committerSon Ho2021-12-07 17:51:47 +0100
commit5b04c0d0475fa8368a361575f7f0084de77ab900 (patch)
tree435e3a71768e0da7d87ea1949af03d731110a9dc /dune-project
parent119de329f565281f5260b00cbc5fb623f6076ed4 (diff)
Update the .gitignore
Diffstat (limited to 'dune-project')
0 files changed, 0 insertions, 0 deletions