diff -r 772a43d88e6b -r 2146cb7be36f tools/rc/to_f64.rs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tools/rc/to_f64.rs	Tue Aug 22 08:35:46 2023 +0200
@@ -0,0 +1,4 @@
+pub fn to_f64<T: Into<f64>>(v: T) -> f64 {
+    v.into()
+}
+