diff --git a/spike/x86/survey.sh b/spike/x86/survey.sh index 85d9da0..8a245f5 100755 --- a/spike/x86/survey.sh +++ b/spike/x86/survey.sh @@ -75,8 +75,12 @@ out=$(mktemp -d); trap 'rm -rf "$out"' EXIT # different lines, so the diff is a report about scheduling rather than about # lowering, and it fails the alias every run. dev-repl outlives the timeout in # the same way and is not listed, because it prints nothing and the two -# truncations are both empty. -forever="dev-loop dev-watch dev-chatty" +# truncations are both empty. agent-auto is here for the dev-loop reason with a +# different clock: its ticks wait on an agent connection that never comes when +# it is run standalone, both backends sit until the timeout, and what each has +# printed by then (a randomized socket path among it) is not a lowering +# comparison. test_agent.ml is where that program's behaviour is asserted. +forever="dev-loop dev-watch dev-chatty agent-auto" # There used to be a second exclusion list here, holding the five dyn # programs, and its note said to take a name off it when the backend grew the