File sync

This page discusses how to set up file sync for files that don’t require full rebuild.

//TODO(#1076)
Last modified March 15, 2019: cut v0.25.0 (#1808) (0f4b8fe)