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 | |
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
-rwxr-xr-x | configure | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -495,7 +495,7 @@ case $usecamlp5 in fi else # Beware of the final \r in Win32 - camlp5dir="$(camlp5 -where | tr -d "\r")" + camlp5dir="$(camlp5 -where | tr -d '\r')" if [ "$camlp5dir" != "" ]; then CAMLP4LIB=$camlp5dir FULLCAMLP4LIB=$camlp5dir @@ -639,8 +639,10 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then else case $lablgtkdir_spec in no) - # Beware of the final \r in Win32 - if lablgtkdirtmp="$(ocamlfind query lablgtk2.sourceview2 2> /dev/null | tr -d "\r")"; then + if lablgtkdirtmp="$(ocamlfind query lablgtk2.sourceview2 2> /dev/null)"; then + # Beware of the final \r in Win32 + # Do not pipe this tr -d above, otherwise the exit code is lost + lablgtkdirtmp="$(echo $lablgtkdirtmp | tr -d '\r')" if [ ! -f "$lablgtkdirtmp/gSourceView2.cmi" ]; then echo "Incomplete Lablgtk2 found by ocamlfind (gSourceView2.cmi not found)." elif [ ! -f "$lablgtkdirtmp/glib.mli" ]; then |