diff options
Diffstat (limited to 'Makefile.nt')
| -rw-r--r-- | Makefile.nt | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Makefile.nt b/Makefile.nt index cfeaac4b52..02e0b1c2df 100644 --- a/Makefile.nt +++ b/Makefile.nt @@ -519,6 +519,14 @@ partialclean:: beforedepend:: asmcomp/selection.ml +asmcomp/CSE.ml: asmcomp/$(ARCH)/CSE.ml + cp asmcomp/$(ARCH)/CSE.ml asmcomp/CSE.ml + +partialclean:: + rm -f asmcomp/CSE.ml + +beforedepend:: asmcomp/CSE.ml + asmcomp/reload.ml: asmcomp/$(ARCH)/reload.ml cp asmcomp/$(ARCH)/reload.ml asmcomp/reload.ml |