Skip to content
Commit f4e420c7 authored by Giovanni Bussi's avatar Giovanni Bussi
Browse files

Hopefully remove harmless error on GitHubActions

Error is this one:
../maketools/makelinks.sh: line 24: echo: write error: Broken pipe

It's triggered by the comparison with a <(echo) file, since the comparison
might fail before echo completes. If this works I will backport it
parent 4aada56d
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment