src/Pure/Admin/component_polyml.scala
changeset 82472 d4b3eea69371
parent 82471 4e63872f3646
child 82473 a69f5be8a33f
equal deleted inserted replaced
82471:4e63872f3646 82472:d4b3eea69371
   104       List("--disable-shared", "--enable-intinf-as-int") :::
   104       List("--disable-shared", "--enable-intinf-as-int") :::
   105         options1 ::: options2 ::: options ::: options3
   105         options1 ::: options2 ::: options ::: options3
   106     }
   106     }
   107 
   107 
   108     platform_context.bash(root,
   108     platform_context.bash(root,
   109       info.setup + "\n" +
   109       Library.make_lines(
   110       """
   110         "set -e",
   111         [ -f Makefile ] && make distclean
   111         info.setup,
   112         {
   112         "[ -f Makefile ] && make distclean",
   113           ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """
   113         """./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
   114           rm -rf target
   114         "rm -rf target",
   115           make && make install
   115         "make",
   116         } || { echo "Build failed" >&2; exit 2; }
   116         "make install"
   117       """, redirect = true).check
   117       ), redirect = true).check
   118 
   118 
   119 
   119 
   120     /* sha1 library */
   120     /* sha1 library */
   121 
   121 
   122     val sha1_files =
   122     val sha1_files =