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