emacs mode should choose HOL executable based on lastmaker file (if any)

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.

https://hol-theorem-prover.org

Other

626 stars 143 forks source link

emacs mode should choose HOL executable based on lastmaker file (if any) #1101

Open mn200 opened 1 year ago

mn200 commented 1 year ago

See #1100 for inspiration.

chenzhawyang commented 1 year ago

i will give it a try when i have time