From 81eec9f92f5cf9c423013cc45438858690fe6280 Mon Sep 17 00:00:00 2001 From: Zoltan Somogyi Date: Fri, 21 Apr 2017 17:12:34 +1000 Subject: [PATCH] Improve the robustness of the INSTALL scripts. .INSTALL.in: INSTALL.git: Generate an error if the name of the current directory contains spaces. .INSTALL.in: Also generate an error if the current directory lacks a boehm_gc subdir, indicating that it is not the result of unpacking a source distribution. Mmakefile: Make INSTALL executable after it is created from .INSTALL.in. (INSTALL.git is already executable.) --- .INSTALL.in | 15 +++++++++++++++ INSTALL.git | 7 +++++++ Mmakefile | 1 + 3 files changed, 23 insertions(+) diff --git a/.INSTALL.in b/.INSTALL.in index 5ee0dc94e..26195acb6 100755 --- a/.INSTALL.in +++ b/.INSTALL.in @@ -95,6 +95,21 @@ # and read the Mercury documentation in the `doc' directory while you are # waiting. +if pwd | grep ' ' +then + echo "The name of the current directory contains spaces." + echo "Mercury cannot be installed from such directories." + exit 1 +fi + +if test ! -d boehm_gc +then + echo "This directory does not contain a complete source distribution." + echo "If you are trying to compile a workspace checked out of git," + echo "you will need to read and follow INSTALL.git, not INSTALL." + exit 1 +fi + sh configure && make && make install diff --git a/INSTALL.git b/INSTALL.git index fce20aceb..f2ee0b143 100755 --- a/INSTALL.git +++ b/INSTALL.git @@ -40,6 +40,13 @@ # If you don't want to do a parallel make, comment out the # `parallel=-j3' line below. +if pwd | grep ' ' +then + echo "The name of the current directory contains spaces." + echo "Mercury cannot be installed from such directories." + exit 1 +fi + parallel=-j3 ./prepare.sh && diff --git a/Mmakefile b/Mmakefile index 30ce87e43..a7d95ae90 100644 --- a/Mmakefile +++ b/Mmakefile @@ -417,6 +417,7 @@ README: .README.in VERSION INSTALL: .INSTALL.in VERSION sed 's/@VERSION@/$(VERSION)/g' .INSTALL.in > INSTALL + chmod a+x INSTALL ifeq ("$(LYNX)","") HTML_TO_TEXT = cat