HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Holmake should deposit last maker files across all directories

Open mn200 opened this issue 4 years ago • 0 comments

The .HOLMK/lastmaker file is created so Holmake (and the emacs mode) can tell which executables to use (useful on machines where multiple HOL installations are present). At the moment, this file is only created in the directory where Holmake is started, which means that attempts to do things in other connected directories can get messed up.

mn200 avatar Feb 17 '21 03:02 mn200