Admin/polyml/README
author blanchet
Wed, 02 Jun 2010 15:18:48 +0200
changeset 37321 9d7cfae95b30
parent 37122 3ac12f743fe5
child 38469 5c6c5d63f3c3
permissions -rw-r--r--
honor "xsymbols"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27012
e6229d8d6aaa moved README-polyml to polyml/README;
wenzelm
parents:
diff changeset
     1
37122
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
     2
This distribution of Poly/ML 5.3 is based on the original
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
     3
polyml.5.3.tar.gz from http://www.polyml.org with some minimal changes:
27012
e6229d8d6aaa moved README-polyml to polyml/README;
wenzelm
parents:
diff changeset
     4
37122
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
     5
diff polyml.5.3/libpolyml/processes.cpp-orig polyml.5.3/libpolyml/processes.cpp
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
     6
995,996c995,996
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
     7
<     // we set this to 100ms so that we're not waiting too long.
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
     8
<     if (maxMillisecs > 100) maxMillisecs = 100;
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
     9
---
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
    10
>     // we set this to 10ms so that we're not waiting too long.
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
    11
>     if (maxMillisecs > 10) maxMillisecs = 10;
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
    12
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
    13
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
    14
Then it is compiled as follows:
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
    15
33540
84380e6c0b1a updated to official Poly/ML 5.3.0;
wenzelm
parents: 28667
diff changeset
    16
  cd polyml.5.3
84380e6c0b1a updated to official Poly/ML 5.3.0;
wenzelm
parents: 28667
diff changeset
    17
  ./configure --prefix="$HOME/tmp/polyml"
27012
e6229d8d6aaa moved README-polyml to polyml/README;
wenzelm
parents:
diff changeset
    18
  make
e6229d8d6aaa moved README-polyml to polyml/README;
wenzelm
parents:
diff changeset
    19
  make install
e6229d8d6aaa moved README-polyml to polyml/README;
wenzelm
parents:
diff changeset
    20
37122
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
    21
33540
84380e6c0b1a updated to official Poly/ML 5.3.0;
wenzelm
parents: 28667
diff changeset
    22
Now $HOME/tmp/polyml/bin/* and $HOME/tmp/polyml/lib/* are moved to the
84380e6c0b1a updated to official Poly/ML 5.3.0;
wenzelm
parents: 28667
diff changeset
    23
platform-specific target directory (e.g. polyml-5.3.0/x86-linux).
27012
e6229d8d6aaa moved README-polyml to polyml/README;
wenzelm
parents:
diff changeset
    24
e6229d8d6aaa moved README-polyml to polyml/README;
wenzelm
parents:
diff changeset
    25
e6229d8d6aaa moved README-polyml to polyml/README;
wenzelm
parents:
diff changeset
    26
	Makarius
37122
3ac12f743fe5 misc updates for release;
wenzelm
parents: 33540
diff changeset
    27
	26-May-2010