aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 3 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index dae6f45f44..aabf09f0ff 100644
--- a/Makefile
+++ b/Makefile
@@ -225,7 +225,7 @@ ML4FILES +=\
contrib/omega/g_omega.ml4 \
contrib/romega/g_romega.ml4 contrib/ring/g_quote.ml4 \
contrib/ring/g_ring.ml4 contrib/dp/g_dp.ml4 \
- contrib/setoid_ring/newring.ml4 \
+ contrib/setoid_ring/newring.ml4 \
contrib/field/field.ml4 contrib/fourier/g_fourier.ml4 \
contrib/extraction/g_extraction.ml4 contrib/xml/xmlentries.ml4
@@ -874,7 +874,8 @@ ZARITHVO=\
theories/ZArith/Zdiv.vo theories/ZArith/Zsqrt.vo \
theories/ZArith/Zwf.vo theories/ZArith/ZArith_base.vo \
theories/ZArith/Zbool.vo theories/ZArith/Zbinary.vo \
- theories/ZArith/Znumtheory.vo theories/ZArith/Int.vo
+ theories/ZArith/Znumtheory.vo theories/ZArith/Int.vo \
+ theories/ZArith/Zpow_def.vo
QARITHVO=\
theories/QArith/QArith_base.vo theories/QArith/Qreduction.vo \
@@ -1754,8 +1755,6 @@ depend: beforedepend dependp4 ml4filesml
done
# 5. We express dependencies of .o files
$(CC) -MM $(CINCLUDES) kernel/byterun/*.c >> .depend
- $(CC) -MM $(CINCLUDES) kernel/byterun/*.c | sed -e 's/\.o/.d.o/' >> \
- .depend
# 6. Finally, we erase the generated .ml files
rm -f $(ML4FILESML)
# 7. Since .depend contains correct dependencies .depend.devel can be deleted