Export/import does not round trip FLOAT values

Copying a table using mysqldump does not preserve FLOAT values precisely. This leads to a checksum mismatch, giving the false impression that the copy has not worked.

The root cause is the fact that FLOAT are stored in MariaDB to more than six significant figures, but mysqldump only outputs six significant figures.

For example, if a FLOAT field is given the value 0.12345678, then mysqldump will write 0.123457 to the file, which when loaded by the new table will be a slightly different value from the original table and the table checksums will be different.

Testing suggests that mysqldump would need to write about 9 significant figures for the FLOAT values to be accurately copied. The problem seems not to occur for DOUBLE values.

Two concrete examples:
Example 1.

CREATE TABLE testtable ( amount FLOAT ) ENGINE Aria;    

INSERT INTO testtable VALUES ( 0.123456789 );

Then export this table using mysqldump to another database. Run CHECKSUM TABLE testtable on each database, and the results will be different.

Example 2.
The following code shows that the checksum only stabilises with around 9 decimal places.

DROP TABLE IF EXISTS testtable6; CREATE TABLE testtable6 ( amount FLOAT ) ENGINE Aria; INSERT INTO testtable6 VALUES (0.123456);

DROP TABLE IF EXISTS testtable7; CREATE TABLE testtable7 ( amount FLOAT ) ENGINE Aria; INSERT INTO testtable7 VALUES (0.1234567);

DROP TABLE IF EXISTS testtable8; CREATE TABLE testtable8 ( amount FLOAT ) ENGINE Aria; INSERT INTO testtable8 VALUES (0.12345678);

DROP TABLE IF EXISTS testtable9; CREATE TABLE testtable9 ( amount FLOAT ) ENGINE Aria; INSERT INTO testtable9 VALUES (0.123456789);

DROP TABLE IF EXISTS testtable10; CREATE TABLE testtable10 ( amount FLOAT ) ENGINE Aria; INSERT INTO testtable10 VALUES (0.1234567891);

DROP TABLE IF EXISTS testtable11; CREATE TABLE testtable11 ( amount FLOAT ) ENGINE Aria; INSERT INTO testtable11 VALUES (0.12345678912);

DROP TABLE IF EXISTS testtable12; CREATE TABLE testtable12 ( amount FLOAT ) ENGINE Aria; INSERT INTO testtable12 VALUES (0.123456789123);

CHECKSUM TABLE testtable6, testtable7, testtable8, testtable9, testtable10, testtable11, testtable12;

Suggestions
Either alter mysqldump so that it outputs more significant figures for FLOAT values, or add an option to mysqldump to allow the user to control the precision.
Or change the way that FLOAT fields are populated, so that they are rounded in a way consistent with mysqldump.