src/Pure/Admin/build_polyml.scala
changeset 67783 839de121665c
parent 67609 738b4d4eeb61
child 69277 258bef08b31e
equal deleted inserted replaced
67782:7e223a05e6d8 67783:839de121665c
   114 
   114 
   115 
   115 
   116     /* configure and make */
   116     /* configure and make */
   117 
   117 
   118     val configure_options =
   118     val configure_options =
   119       List("--enable-intinf-as-int", "--with-gmp") ::: info.platform_options(arch_64) ::: options
   119       List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") :::
       
   120         info.platform_options(arch_64) ::: options
   120 
   121 
   121     bash(root,
   122     bash(root,
   122       info.setup + "\n" +
   123       info.setup + "\n" +
   123       """
   124       """
   124         [ -f Makefile ] && make distclean
   125         [ -f Makefile ] && make distclean