diff --git a/wiki/tools.md b/wiki/tools.md index 4c00d968a..03e137563 100644 --- a/wiki/tools.md +++ b/wiki/tools.md @@ -581,6 +581,12 @@ match no entry. Both land in the `--json` report (`new_files`, with since the pin or an undeclared hash makes the profile stale. `--tree-diff` shows added, removed and renamed files in the directories the refs point at. +Branch tips, tags and releases are cached for six hours. `--fresh` asks the +forges again for them, which matters right after an upstream commit or a +hand-set pin: a tip cached before the pin reads as behind it. It is refused +with `--offline`. A run that writes a profile also rebuilds the site's record +of cited source paths (`website/src/data/source-paths.json`). + Writes are explicit and mechanical only. `--backfill-commits` fills a missing `source_commit`, `--rebase-refs` recales `SHIFTED` and `RENAMED` line ranges and moves `source_commit` to HEAD with them, all or nothing,