aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2016-11-13 22:32:38 -0500
committerGravatar Andres Erbsen <andreser@mit.edu>2016-11-13 22:32:38 -0500
commit3049b95b62e80cb15a203879a5a610aa720aae4a (patch)
tree70a60c9c9d4a7c19e055e2377450bfdcd68a9737 /Makefile
parentb62e43415047671f2b7e33ca8b819fe0e52487b2 (diff)
Proper_sqrt
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 18cda2236..449f5fe98 100644
--- a/Makefile
+++ b/Makefile
@@ -110,7 +110,7 @@ src/Experiments/X25519.o: src/Experiments/X25519.hs
( cd src/Experiments && ghc -XStrict -O3 X25519.hs )
extraction: src/Experiments/Ed25519.hs src/Experiments/X25519.hs
-ghc: src/Experiments/Ed25519.core src/Experiments/Ed25519.o src/Experiments/X25519.o src/Experiments/X25519.core
+ghc: src/Experiments/Ed25519.o src/Experiments/X25519.o
clean::
rm -f Makefile.coq