diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-30 13:42:25 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-30 13:42:34 +0200 |
commit | 0d5abcf9e17b4fe0462ffa60d04a321d2707ccf6 (patch) | |
tree | ff11ee436493d8516d22af084171c41fc1079a15 /Makefile.dev | |
parent | 58107b74ba65947129aff8203a821d146ecd18ac (diff) |
Missing .PHONY targets.
Diffstat (limited to 'Makefile.dev')
-rw-r--r-- | Makefile.dev | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dev b/Makefile.dev index 501a7744a..1f81edc2c 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -167,7 +167,7 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ .PHONY: init theories-light noreal .PHONY: logic arith bool narith zarith qarith lists strings sets .PHONY: fsets relations wellfounded reals setoids sorting numbers -.PHONY: msets mmaps compat +.PHONY: msets mmaps compat parith classes program unicode structures vectors ################ ### 4) plugins |