From 692c81477601cb09401f8be3dfba41ca3d04780f Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Tue, 17 Nov 2020 09:26:03 -0800
Subject: [PATCH] Don't add an extra copy of Programming Cryptol (#970)

Two different Makefiles each copied it and used different file names.

Closes #969.
---
 docs/ProgrammingCryptol/Makefile | 1 -
 1 file changed, 1 deletion(-)

diff --git a/docs/ProgrammingCryptol/Makefile b/docs/ProgrammingCryptol/Makefile
index 433d7d16..c7301cfe 100644
--- 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