Commit 70dc5de
committed
ocamlyices2: use --without-gmp-embedded by default
After giving it some thoughts, the need for having a self-contained libyices.a
(which would only need -lyices, no -lgmp needed) in ocamlyices2 is pointless
as 'zarith' will still need '-lgmp' anyway.
The Makefile will still put libgmp.a and libyices.a inside src/ so that
the static version of gmp is used (with -L.) instead of the shared version.
Rationale: disabling the partial linking fixes the build on Arch Linux, which
(I re-tested on a docker image) cannot accept partial linking with -lgmp when
only libgmp.so is available. Here is the failing command:
ld -r *.o -lgmp -o libyices.o1 parent df7c89a commit 70dc5de
2 files changed
Lines changed: 15 additions & 18 deletions
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1387 | 1387 | | |
1388 | 1388 | | |
1389 | 1389 | | |
1390 | | - | |
1391 | | - | |
1392 | | - | |
1393 | | - | |
1394 | | - | |
1395 | | - | |
1396 | | - | |
| 1390 | + | |
| 1391 | + | |
| 1392 | + | |
| 1393 | + | |
| 1394 | + | |
| 1395 | + | |
1397 | 1396 | | |
1398 | 1397 | | |
1399 | 1398 | | |
| |||
4040 | 4039 | | |
4041 | 4040 | | |
4042 | 4041 | | |
4043 | | - | |
| 4042 | + | |
4044 | 4043 | | |
4045 | | - | |
| 4044 | + | |
4046 | 4045 | | |
4047 | 4046 | | |
4048 | 4047 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
118 | 118 | | |
119 | 119 | | |
120 | 120 | | |
121 | | - | |
122 | | - | |
123 | | - | |
124 | | - | |
125 | | - | |
126 | | - | |
127 | | - | |
128 | | - | |
129 | | - | |
| 121 | + | |
| 122 | + | |
| 123 | + | |
| 124 | + | |
| 125 | + | |
| 126 | + | |
| 127 | + | |
130 | 128 | | |
131 | 129 | | |
132 | 130 | | |
| |||
0 commit comments