diff options
| author | Gaëtan Gilbert | 2018-11-09 19:27:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-20 13:02:04 +0100 |
| commit | d7172fbf2d7ae98ea0471a58c21f93671280d50e (patch) | |
| tree | 0da78b3ce4563460b245eb641acb3d911fd85390 /dev/dune-dbg.in | |
| parent | 4d26550af26c1dab464253cc470e8a876fee0025 (diff) | |
Fix dune-dbg using checker/main -> checker/coqchk
Diffstat (limited to 'dev/dune-dbg.in')
| -rwxr-xr-x | dev/dune-dbg.in | 2 |
1 files changed, 1 insertions, 1 deletions
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 |