diff options
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 742395422..f333ae63e 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v fi; \ } > "$@" -# Additionnal dependencies for module tests +# Additional dependencies for module tests $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo modules/%.vo: modules/%.v $(HIDE)$(coqtop) -R modules Mods -compile $< |