Opened 3 years ago

Last modified 3 years ago

#509 new defect

isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined.

Reported by: coquser Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-4.3
Component: 2:pg-emacs Keywords: make compile
Cc:

Description

I searched and found the same error reported already as Ticket #500. It was marked as closed. However I downloaded the latest PG (4.2) and got the same error. Has the fix been applied to that version?

Details follow:

I am a new PG user on Mac OS X El Capitan Version 10.11.3 (15D21) GNU Emacs 24.5.1 (x86_64-apple-darwin13.4.0, NS apple-appkit-1265.21) of 2015-04-10 on builder10-9.porkrind.org Proof General 4.2

After installation I opened a Coq file and was told that I needed to recompile because my Emacs was a later version. I ran: make clean; make compile EMACS=/Applications/Emacs?.app/Contents/MacOS/Emacs

At the end 2 errors were reported:

In toplevel form: isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined. make[1]: * [isar/isar-unicode-tokens.elc] Error 1 make: * [compile] Error 2

Change History (1)

comment:1 Changed 3 years ago by coquser

I downloaded the prerelease version ProofGeneral-4.3pre150930.tgz from the Development page. The error is fixed. Close this ticket.

Note: See TracTickets for help on using tickets.