for consistency also rename floats.rs

This commit is contained in:
Ralf Jung 2020-03-30 13:39:04 +02:00
parent ab32084ddb
commit 41abcdb422