diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-11-21 22:47:14 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2013-11-21 23:01:53 +0100 |
| commit | b3bc0e3a3289314baf95d948578ca4ee51a9db94 (patch) | |
| tree | 8e5bfe6bbce33ef01d8b8bf23fd2eab09ac825f9 /library/libobject.ml | |
| parent | 71bd17b666e82ffb2b83644e5c122763e12e900b (diff) | |
configure: fix some issues with last commit
- after piping with | tr -d, an exit code was lost
- suspicious use of " " inside a larger " ", we use ' ' now instead
Diffstat (limited to 'library/libobject.ml')
0 files changed, 0 insertions, 0 deletions