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.

REDUCE Historical
REDUCE Sourceforge Project | Historical SVN Repository | GitHub Mirror | SourceHut Mirror | NotABug Mirror | Chisel Mirror | Chisel RSS ]