Change the naming convention for extension files to use double dashes.

Change the naming convention for extension files to use double dashes.

This allows us to have an unambiguous rule for deconstructing the names
of script files and secondary control files, without having to forbid
extension and version names from containing any dashes.  We do have to
forbid them from containing double dashes or leading/trailing dashes,
but neither restriction is likely to bother anyone in practice.
Per discussion, this seems like a better solution overall than the
original design.