equal
deleted
inserted
replaced
1 Poly/ML for Isabelle |
1 Poly/ML for Isabelle |
2 ==================== |
2 ==================== |
3 |
3 |
4 This compilation of Poly/ML 5.6 (http://www.polyml.org) is based on the source |
4 This compilation of Poly/ML 5.6 (http://www.polyml.org) is based on the source |
5 distribution from https://github.com/polyml/polyml/releases/tag/v5.6/. |
5 distribution from https://github.com/polyml/polyml/releases/tag/v5.6/. |
|
6 |
|
7 On Linux the sources have changed as follows, in order to evade a |
|
8 potential conflict of /bin/bash versus /bin/sh -> dash (notably on |
|
9 Ubuntu and Debian): |
|
10 |
|
11 diff -r src-orig/libpolyml/process_env.cpp src/libpolyml/process_env.cpp |
|
12 228c228 |
|
13 < execve("/bin/sh", argv, environ); |
|
14 --- |
|
15 > execvp("bash", argv); |
|
16 |
6 |
17 |
7 The included build script is used like this: |
18 The included build script is used like this: |
8 |
19 |
9 ./build src x86-linux --with-gmp |
20 ./build src x86-linux --with-gmp |
10 ./build src x86_64-linux --with-gmp |
21 ./build src x86_64-linux --with-gmp |
16 Also note that the separate "sha1" library module is required for |
27 Also note that the separate "sha1" library module is required for |
17 efficient digestion of strings according to SHA-1. |
28 efficient digestion of strings according to SHA-1. |
18 |
29 |
19 |
30 |
20 Makarius |
31 Makarius |
21 31-Jan-2016 |
32 11-Feb-2016 |