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' \