Opened 8 years ago
Last modified 8 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
I downloaded the prerelease version ProofGeneral-4.3pre150930.tgz from the Development page. The error is fixed. Close this ticket.