Skip to content

Replace outdated macro (removed in dune 2.10)#796

Closed
timokoch wants to merge 1 commit intoOPM:masterfrom timokoch:patch-1
+1-1

Commits

Commits on Nov 6, 2024