Disambiguate names of timer drivers

Issue #2190
2026-01-21 12:32:56 +01:00 · 2016-12-10 23:22:13 +01:00
parent f54c85e045
commit 44df8db771
37 changed files with 57 additions and 71 deletions
--- a/tool/run/boot_dir/linux
+++ b/tool/run/boot_dir/linux
@@ -1,4 +1,5 @@
 proc binary_name_ld_lib_so { } { return "ld-linux.lib.so" }
+proc binary_name_timer     { } { return "linux_timer_drv" }


 ##