aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2013-11-09 18:50:59 -0500
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2013-11-21 21:23:43 +0100
commit71bd17b666e82ffb2b83644e5c122763e12e900b (patch)
tree2f6370c87cbcebadd06f6b464fce825a0d68ea58
parentb7a1511c0841c15a8919d409ea4a4893e623b43a (diff)
Fix various \r issues with windows
Also add a 2 in an error message (it's gSourceView2, not gSourceView). This closes bugs 3150, 3151, 3152, and 3153.
-rwxr-xr-xconfigure11
1 files changed, 7 insertions, 4 deletions
diff --git a/configure b/configure
index 1a6b72604..1e0290b7f 100755
--- a/configure
+++ b/configure
@@ -336,7 +336,8 @@ fi
MAKE=`which ${makecmd:-make}`
if [ "$MAKE" != "" ]; then
- MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
+ # Beware of the final \r in Win32
+ MAKEVERSION=`"$MAKE" -v | head -1 | tr -d "\r" | cut -d" " -f3`
MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
if [ "$MAKEVERSIONMAJOR" -gt 3 -o "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
@@ -493,7 +494,8 @@ case $usecamlp5 in
exit 1
fi
else
- camlp5dir="$(camlp5 -where)"
+ # Beware of the final \r in Win32
+ camlp5dir="$(camlp5 -where | tr -d "\r")"
if [ "$camlp5dir" != "" ]; then
CAMLP4LIB=$camlp5dir
FULLCAMLP4LIB=$camlp5dir
@@ -637,9 +639,10 @@ 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
+ if lablgtkdirtmp="$(ocamlfind query lablgtk2.sourceview2 2> /dev/null | tr -d "\r")"; then
if [ ! -f "$lablgtkdirtmp/gSourceView2.cmi" ]; then
- echo "Incomplete Lablgtk2 found by ocamlfind (gSourceView.cmi not found)."
+ echo "Incomplete Lablgtk2 found by ocamlfind (gSourceView2.cmi not found)."
elif [ ! -f "$lablgtkdirtmp/glib.mli" ]; then
echo "Incomplete Lablgtk2 found by ocamlfind (glib.mli not found)."
else