aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2013-11-22 10:23:35 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2013-11-22 10:25:58 +0100
commit1abae19d5688b987b19efba8bcac8577892fcd27 (patch)
tree185481db06908e0f430ded68c12480f275c3476f
parenta9f32885991263cf17093c6959732a339d473b45 (diff)
configure: improve last fix
Let's avoid the "if a=$(cmd ...)" since: - unless being a shell expert, it's not obvious it's testing the exit code of cmd. - it's quite fragile, if you pipe cmd into a cmd2 you'll lose the exit code of cmd. Instead, we test the emptiness of the variable content afterwards
-rwxr-xr-xconfigure7
1 files changed, 3 insertions, 4 deletions
diff --git a/configure b/configure
index 088d7e501..dbf6c8093 100755
--- a/configure
+++ b/configure
@@ -639,10 +639,9 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then
else
case $lablgtkdir_spec in
no)
- 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')"
+ # Beware of the final \r in Win32
+ lablgtkdirtmp="$(ocamlfind query lablgtk2.sourceview2 2> /dev/null | tr -d '\r')"
+ if [ "$labgtkdirtmp" != "" ]; then
if [ ! -f "$lablgtkdirtmp/gSourceView2.cmi" ]; then
echo "Incomplete Lablgtk2 found by ocamlfind (gSourceView2.cmi not found)."
elif [ ! -f "$lablgtkdirtmp/glib.mli" ]; then