aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2013-11-21 22:47:14 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2013-11-21 23:01:53 +0100
commitb3bc0e3a3289314baf95d948578ca4ee51a9db94 (patch)
tree8e5bfe6bbce33ef01d8b8bf23fd2eab09ac825f9
parent71bd17b666e82ffb2b83644e5c122763e12e900b (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-xconfigure8
1 files changed, 5 insertions, 3 deletions
diff --git a/configure b/configure
index 1e0290b7f..a05548e38 100755
--- a/configure
+++ b/configure
@@ -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