Mentions légales du service

Skip to content
Snippets Groups Projects
Forked from The Rocq Prover / The Rocq Prover
Source project has a limited visibility.
  • Emilio Gallego's avatar
    4d966c45
    [build] Set dune root explicitly / use --release · 4d966c45
    Emilio Gallego authored
    This should fix #14915 , the problem arises with layouts of the form:
    
    ```
    foo/dune-project
    foo/_opam/bar/dune-project
    ```
    
    so when inside `foo/_opam/bar`, dune will switch to `foo` as the
    project root, for example for `dune build` or `dune exec` , however,
    as `_opam` is an ignored dir by default in the `foo` context, the
    command will fail.
    
    So indeed, it turns out `--profile release` is not enough, but
    `--release` must be used when configured for install.
    
    Thanks a lot to Kate for the help!
    4d966c45
    History
    [build] Set dune root explicitly / use --release
    Emilio Gallego authored
    This should fix #14915 , the problem arises with layouts of the form:
    
    ```
    foo/dune-project
    foo/_opam/bar/dune-project
    ```
    
    so when inside `foo/_opam/bar`, dune will switch to `foo` as the
    project root, for example for `dune build` or `dune exec` , however,
    as `_opam` is an ignored dir by default in the `foo` context, the
    command will fail.
    
    So indeed, it turns out `--profile release` is not enough, but
    `--release` must be used when configured for install.
    
    Thanks a lot to Kate for the help!