diff options
| author | Enrico Tassi | 2018-05-02 11:17:54 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-05-02 11:17:54 +0200 |
| commit | 0057815355ae6a276028e5997e6fe841e41c3983 (patch) | |
| tree | dfa96374d7826f17bc9277b0dd05dff4e05a44bc /tools | |
| parent | a9b4d88ff0f403ea3503f1c5eedc4959ce4c2e30 (diff) | |
| parent | aa681a064cf15f3aeb55fde48dfe049d39e4065f (diff) | |
Merge PR #7370: Fix PHONY typo in coq_makefile
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f6539d80be..e5f22f25e1 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -382,7 +382,7 @@ real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) .PHONY: real-all real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) -.PHONE: real-all.timing.diff +.PHONY: real-all.timing.diff bytefiles: $(CMOFILES) $(CMAFILES) .PHONY: bytefiles |