src/Pure/Admin/build_polyml.scala
changeset 74635 b179891dd357
parent 73672 70d3c7009a65
child 75202 4fdde010086f
equal deleted inserted replaced
74634:8f7f626aacaa 74635:b179891dd357
    87       """
    87       """
    88         [ -f Makefile ] && make distclean
    88         [ -f Makefile ] && make distclean
    89         {
    89         {
    90           ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
    90           ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
    91           rm -rf target
    91           rm -rf target
    92           make compiler && make compiler && make install
    92           make && make install
    93         } || { echo "Build failed" >&2; exit 2; }
    93         } || { echo "Build failed" >&2; exit 2; }
    94       """, redirect = true, echo = true).check
    94       """, redirect = true, echo = true).check
    95 
    95 
    96 
    96 
    97     /* sha1 library */
    97     /* sha1 library */