Don't add an extra copy of Programming Cryptol (#970)

Two different Makefiles each copied it and used different file names. Closes #969.
GaloisInc · Nov 17, 2020 · 692c814 · 692c814
1 parent 85413b3
commit 692c814
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/docs/ProgrammingCryptol/Makefile b/docs/ProgrammingCryptol/Makefile
@@ -25,7 +25,6 @@ MAKEINDEX = makeindex
 # TODO: Ensure that TEXINPUTS is set correctly to make \includes and \usepackages more robust?
 
 all: pdf
-	cp ${TMP}/Cryptol.pdf ..
 
 test:
 	cd aes ; make test