diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-30 12:32:53 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-30 12:35:58 -0400 |
| commit | 192fe7b7b7cc552fcdfa36015aeb8f2498f65b74 (patch) | |
| tree | 4da25d6418830a0d9e136db942d18265a588827f /test-suite/Makefile | |
| parent | fd36c0451c26e44b1b7e93299d3367ad2d35fee3 (diff) | |
Fix empty parentheses display in test-suite
There was an extra trailing space in #680.
Now things display as, e.g.,
```
TEST bugs/opened/3754.v
TEST bugs/opened/4803.v (-compat 8.4)
```
instead of
```
TEST bugs/opened/3754.v ( )
TEST bugs/opened/4803.v (-compat 8.4 )
```
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 285460762..ba706a297 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -45,7 +45,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) # read out an emacs config and look for coq-prog-args; if such exists, return it get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1) -get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) +get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) SINGLE_QUOTE=" #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter # wrap the arguments in parens, but only if they exist |