diff options
| author | Pierre Roux | 2019-11-10 16:12:04 +0100 |
|---|---|---|
| committer | Pierre Roux | 2019-11-11 17:43:23 +0100 |
| commit | 09b39c339dd3fe21a0808097b5f7d1ab8cb47031 (patch) | |
| tree | 40eb1aa01c8ffbc4531c5a4227c07d50b8051bdb /configure.ml | |
| parent | 69b91851ed5d18f1ca34ef2597f0cf342c10a124 (diff) | |
Have only one dune rule calling configure
Diffstat (limited to 'configure.ml')
| -rw-r--r-- | configure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml index a53292b4cf..411578445c 100644 --- a/configure.ml +++ b/configure.ml @@ -1216,7 +1216,7 @@ let write_dune_c_flags f = close_out o; Unix.chmod f 0o444 -let _ = try write_dune_c_flags "kernel/byterun/dune.c_flags" with _ -> () +let _ = write_dune_c_flags "config/dune.c_flags" let write_macos_metadata exec = let f = "config/Info-"^exec^".plist" in |