aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-05-25 12:21:48 -0400
committerGravatar Paul Steckler <steck@stecksoft.com>2017-05-25 12:21:48 -0400
commitcde87048ee6074e203db8b062740bec0be9484d2 (patch)
tree9536816ccc7184c5267fe263fc4b8b88cdc5008a /test-suite/Makefile
parent9c8cdd5f6c1cb4bda2f8558c17df3ffe69c49264 (diff)
add Show test with -emacs flag
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index c2d6e540c..b627f680b 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 $(filter-out "-emacs-U" "-emacs",$(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
@@ -490,7 +490,7 @@ coq-makefile/%.log : coq-makefile/%/run.sh
$(HIDE)(\
cd coq-makefile/$* && \
./run.sh 2>&1; \
- if [ $$? = 0 ]; then \
+ if [ $$? = 0 ]; then \
echo $(log_success); \
echo " $<...Ok"; \
else \