diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-07-08 12:36:45 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-07-08 12:36:45 -0400 |
| commit | a44b4be1bf8b96e941216cd10cfb5981a825c3fa (patch) | |
| tree | 033fbe56cd25893bf3b87399dc27e2dcf79dcc1c /tools/CoqMakefile.in | |
| parent | 39ba36bfa1ee2aa951dbad9f518bde81e45f3e9d (diff) | |
| parent | b0e406ba35be96b525c631f8d1899e5e9eeb0a91 (diff) | |
Merge PR #8015: Output UTF-8 explicitly in timing tools
Diffstat (limited to 'tools/CoqMakefile.in')
| -rw-r--r-- | tools/CoqMakefile.in | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 872a73282..8b6822a4e 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -90,9 +90,9 @@ COQDOC ?= "$(COQBIN)coqdoc" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts -COQMAKE_ONE_TIME_FILE ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-one-time-file.py" -COQMAKE_BOTH_TIME_FILES ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-both-time-files.py" -COQMAKE_BOTH_SINGLE_TIMING_FILES ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-both-single-timing-files.py" +COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" BEFORE ?= AFTER ?= |