HOL
HOL copied to clipboard
Holmake should deposit last maker files across all directories
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.