diff tools/verify-all-heads.sh @ 1498:cf82df69b794

Merge default heads. Cleaned up some comments in wrappers as a result of duplicate work. Sigh.
author Augie Fackler <raf@durin42.com>
date Sun, 12 Feb 2017 16:35:08 -0500
parents 11c4c7242a36
children
line wrap: on
line diff