that wasn't a comment char apparently

GaloisInc · Apr 9, 2018 · b4d8b55 · b4d8b55
1 parent 7f53c82
commit b4d8b55
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/configure b/configure
@@ -9,7 +9,7 @@ source script/coqproject.sh
 make Makefile.coq 2> /dev/null
 mv Makefile.coq Makefile.coq.src
 
-DIRS=(src HMAC verif)# SHA256 otp)
+DIRS=(src HMAC verif)
 source script/coqproject.sh
 
 make Makefile.coq 2> /dev/null