summaryrefslogtreecommitdiff
path: root/dune-project
diff options
context:
space:
mode:
authorAkshay <[email protected]>2021-08-10 16:54:15 +0100
committerAkshay <[email protected]>2021-08-10 16:54:15 +0100
commit904e52663bcc2953fdac8706752e928f5ed0cecd (patch)
tree91d8399fbca61e0358d5faf4468d25af1f056be1 /dune-project
parent08e90070acd6b00ad970caf5c0a2f36c9ea07a5c (diff)
devshell messes up dune utopmain
Diffstat (limited to 'dune-project')
0 files changed, 0 insertions, 0 deletions