diff options
| author | Pierre-Marie Pédrot | 2018-11-21 13:06:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-21 13:06:23 +0100 |
| commit | e0db7f1baef37bb60db2dd1c963572f175392783 (patch) | |
| tree | 8fc59a2d77d5cd32622c5a4f2071d22abee5a78f /dev | |
| parent | 4d0fea2ededb11d79f4f1abcc1595f9cec20d6dd (diff) | |
| parent | 7aeddf5cbf5755dab1cdcbab832c3d51a02c6c84 (diff) | |
Merge PR #8961: dune: link kernel in checker instead of copying files
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/dune | 2 | ||||
| -rwxr-xr-x | dev/dune-dbg.in | 2 |
2 files changed, 2 insertions, 2 deletions
@@ -10,7 +10,7 @@ (rule (targets dune-dbg) (deps dune-dbg.in - ../checker/main.bc + ../checker/coqchk.bc ../topbin/coqtop_byte_bin.bc ; This is not enough as the call to `ocamlfind` will fail :/ top_printers.cma) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 3f3df23fe1..80ad0500e0 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -3,7 +3,7 @@ # Run in a proper install dune env. case $1 in checker) - exe=_build/default/checker/main.bc + exe=_build/default/checker/coqchk.bc ;; *) exe=_build/default/topbin/coqtop_byte_bin.bc |
