From ad9aa9fa70ea9e4bc525f0b8ea2b06c8c4395535 Mon Sep 17 00:00:00 2001 From: Connor Olding Date: Tue, 18 Oct 2022 13:45:55 -0700 Subject: [PATCH] yices: rewrite comment --- cosmo-yices/Dockerfile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/cosmo-yices/Dockerfile b/cosmo-yices/Dockerfile index d676034..0f96d13 100644 --- a/cosmo-yices/Dockerfile +++ b/cosmo-yices/Dockerfile @@ -60,9 +60,9 @@ RUN : \ COPY --from=downloader /gmp /gmp WORKDIR /gmp RUN : \ -# don't build this crap. our printf is fine. \ -# (i suppose this cause linking issues further down the \ -# line, but yices is fine without any of these symbols.) \ +# don't build this crap; our printf is fine. \ +# (i suppose the missing symbols could cause linking errors further \ +# down the line, but this does not seem to be an issue for yices.) \ && rm -r printf \ && shed configure 's_ printf/Makefile _ _g' '/printf\/Makefile/d' \ && shed Makefile.in 's_ printf _ _g' 's/$(PRINTF_OBJECTS) //g' \