id,summary,reporter,owner,description,type,status,priority,milestone,component,resolution,keywords,cc 509,isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined.,coquser,David Aspinall,"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",defect,new,minor,PG-Emacs-4.3,2:pg-emacs,,make compile,