diff options
author | Nadrieril | 2024-05-22 15:10:50 +0200 |
---|---|---|
committer | Guillaume Boisseau | 2024-05-24 14:24:38 +0200 |
commit | b66f7fee37bf2127e07b0865edb8fb1e039cab9e (patch) | |
tree | f2bc1ab8b09cabd68aff7ff8572057910e0dc7b1 /compiler/Pure.ml | |
parent | 88a2112b3561eff8b6996d740b5c0e1f62c2d9ee (diff) |
make: deduplicate setting the backend
Diffstat (limited to 'compiler/Pure.ml')
0 files changed, 0 insertions, 0 deletions