# HG changeset patch # User Adam Chlipala # Date 1222905191 14400 # Node ID de9f78d68053a9e7074afc160623960c3cc3e778 # Parent 943478e5a32de5510b225d4a70ffa8f69abe1792 Publish to Harvard, too diff -r 943478e5a32d -r de9f78d68053 Makefile --- a/Makefile Wed Oct 01 10:07:14 2008 -0400 +++ b/Makefile Wed Oct 01 19:53:11 2008 -0400 @@ -61,4 +61,5 @@ cp cpdt.tgz staging/ cp latex/cpdt.pdf staging/ cp -R html staging/ + rsync -az --exclude '*~' staging/* bowser.eecs.harvard.edu:public_html/cpdt/book/ rsync -az --exclude '*~' staging/* ssh.hcoop.net:sites/chlipala/adam/cpdt/ diff -r 943478e5a32d -r de9f78d68053 staging/index.html --- a/staging/index.html Wed Oct 01 10:07:14 2008 -0400 +++ b/staging/index.html Wed Oct 01 19:53:11 2008 -0400 @@ -4,7 +4,7 @@ Certified Programming with Dependent Types

Certified Programming with Dependent Types

Adam Chlipala

This is the web site for an in-progress textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.