summaryrefslogtreecommitdiff
path: root/compiler/dune
diff options
context:
space:
mode:
authorSon Ho2023-10-25 11:40:31 +0200
committerSon Ho2023-10-25 11:40:31 +0200
commitece74df70f12790bab7ecfe0c590c2c637e89801 (patch)
treedaee3bda9d393c33942b8cdcb6a7d975ad275f05 /compiler/dune
parent9c230dddebb171ee1b3e0176838441163836b875 (diff)
Update following the addition of raw pointers
Diffstat (limited to '')
-rw-r--r--compiler/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/dune b/compiler/dune
index 4ec46b70..a4b09df4 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -92,4 +92,4 @@
-g
;-dsource
-warn-error
- -5-8-9-11-14-33-20-21-26-27-39)))
+ -5@8-9-11-14-33-20-21-26-27-39)))