Reviewers: lemzwerg, Message: On 2020/02/22 22:01:10, lemzwerg wrote: > Never seen such code before, but if it fixes an issue... :-)
it's a cut and paste from the internet, https://blog.apokalyptik.com/2007/10/24/bash-tip-closing-file-descriptors/ I'm surprised that make passes on the console stdin to child processes, but it does appear to happen. Description: run-and-check: close stdin This stops pdflatex hanging, waiting for console input. Please review this at https://codereview.appspot.com/545620043/ Affected files (+3, -0 lines): M scripts/build/run-and-check.sh Index: scripts/build/run-and-check.sh diff --git a/scripts/build/run-and-check.sh b/scripts/build/run-and-check.sh index 5453821c1eebae19e51a0fa97e9f7cb54549e1b1..fc78a4756f60771a53dfe85939f9741d6247c8bd 100755 --- a/scripts/build/run-and-check.sh +++ b/scripts/build/run-and-check.sh @@ -4,6 +4,9 @@ # parameter 1 could contain a directory change. CurrDir=`pwd` +# Make sure nobody tries to read console input +exec 0>&- # close stdin + # The next code line takes the value in parameter 1, evaluates # it (necessary if it contains spaces), and runs it. #
