Re: [PD-dev] double precision merged (was: PRs for 0.51)