The "mtime-changes" setting:

Use file modification times (mtimes) to detect when files have been modified. If disabled, all managed files are hashed to detect changes, which can be slow for large projects.

GRG for REDUCE
GRG Homepage | GitHub Mirror | SourceHut Mirror | NotABug Mirror | Chisel Mirror | Chisel RSS ]