diff options
Diffstat (limited to 'tools/command-lines-input.sh')
| -rwxr-xr-x | tools/command-lines-input.sh | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/tools/command-lines-input.sh b/tools/command-lines-input.sh deleted file mode 100755 index 3e0dafb44..000000000 --- a/tools/command-lines-input.sh +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/bash - -cat command-lines.in | grep -v '^#' | grep -v '\-\-\-' | grep -v '^$' > command-lines.tmp -echo "" >> command-lines.tmp -echo "const char _command_input[] =" > command-lines-input.h -while read -r line; do - echo "" >> command-lines-input.h - printf '\"%s\\n\"' "$line" >> command-lines-input.h -done < command-lines.tmp -echo ";" >> command-lines-input.h - |