hg: drop pointless push_ssl configuration setting - if there is a risk push can be compromised, credentials can also easily be stolen for pull Everybody should have a ssl-only setup now. Alternatively, there is a use case for 'only anonymous traffic on ssl - all authentication and authenticated traffic must be on ssl'. That can be done with proper web server configuration.