yices: rewrite comment
This commit is contained in:
parent
efd9608d42
commit
ad9aa9fa70
1 changed files with 3 additions and 3 deletions
|
@ -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' \
|
||||
|
|
Loading…
Reference in a new issue