Opened 8 years ago
Closed 8 years ago
#512 closed defect (fixed)
test.coq target doesn't exist
| Reported by: | coquser | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.3 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: |
Description
In the coq subdirectory of PG, there's a file coq-autotest.el. In that file:
;; coq-autotest.el: tests of Coq Proof General (in progress). ;; You can run these by issuing "make test.coq" in PG home dir.
That target does not exist in the main directory's Makefile.
That behavior holds in PG 4.2 as well as the 4.3 preview I downloaded, 4.3pre150930.
Note: See
TracTickets for help on using
tickets.
Target exists in 4.4pre on github, so closing.