max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(tests/lean/interactive/mk_input): strip \r from input files (win)

Browse source
This commit is contained in:
Mario Carneiro 2017-06-21 02:24:51 -04:00 • committed by Gabriel Ebner
parent eef4d95410
commit e6f3c5cc22
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
tests/lean/interactive/mk_input.sh
View file

@ -2,6 +2,7 @@
# generate server input from "--^" markers
INPUT="$(cat)"
ESC_INPUT="${INPUT//$'\n'/\\n}"
ESC_INPUT="${ESC_INPUT//$'\r'/}"
ESC_INPUT="${ESC_INPUT//\"/\\\"}"
echo "{\"seq_num\": 0, \"command\": \"sync\", \"file_name\": \"f\", \"content\": \"$ESC_INPUT\"}"
awk '{