From adf39c4cc891bab6c84f92194b6c6966827db599 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Josef=20S=C3=B6ntgen?= Date: Wed, 29 Mar 2017 13:46:54 +0200 Subject: [PATCH] autopilot: remove unused default_log_file proc --- tool/autopilot | 1 - 1 file changed, 1 deletion(-) diff --git a/tool/autopilot b/tool/autopilot index bed6216c3..1a6bd3494 100755 --- a/tool/autopilot +++ b/tool/autopilot @@ -35,7 +35,6 @@ proc genode_dir { } { proc default_test_dir { } { global env; return "/tmp/autopilot.$env(USER)" } -proc default_log_file { } { return "autopilot.log" } ##