Opened 4 years ago

Closed 4 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:


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.

Change History (1)

comment:1 Changed 4 years ago by coquser

Resolution: fixed
Status: newclosed

Target exists in 4.4pre on github, so closing.

Note: See TracTickets for help on using tickets.