From 548e62be073aa5a7b39d5826cd72681daef7c6a1 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 28 Dec 2020 15:48:35 +0100
Subject: configure: simplify the final printing of the configuration

Factor out the substitution of `$prefix` for `\$(PREFIX)`
using a shell function `expandprefix`.
---
 configure | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

(limited to 'configure')

diff --git a/configure b/configure
index b0d57823..ac41ab56 100755
--- a/configure
+++ b/configure
@@ -803,10 +803,9 @@ Please finish the configuration by editing file ./Makefile.config.
 EOF
 else
 
-bindirexp=`echo "$bindir" | sed -e "s|\\\$(PREFIX)|$prefix|"`
-libdirexp=`echo "$libdir" | sed -e "s|\\\$(PREFIX)|$prefix|"`
-mandirexp=`echo "$mandir" | sed -e "s|\\\$(PREFIX)|$prefix|"`
-coqdevdirexp=`echo "$coqdevdir" | sed -e "s|\\\$(PREFIX)|$prefix|"`
+expandprefix() {
+  echo "$1" | sed -e "s|\\\$(PREFIX)|$prefix|"
+}
 
 cat <<EOF
 
@@ -828,17 +827,17 @@ CompCert configuration:
     Menhir API library............ $menhir_dir
     The Flocq library............. $library_Flocq
     The MenhirLib library......... $library_MenhirLib
-    Binaries installed in......... $bindirexp
+    Binaries installed in......... $(expandprefix $bindir)
     Runtime library provided...... $has_runtime_lib
-    Library files installed in.... $libdirexp
-    Man pages installed in........ $mandirexp
+    Library files installed in.... $(expandprefix $libdir)
+    Man pages installed in........ $(expandprefix $mandir)
     Standard headers provided..... $has_standard_headers
-    Standard headers installed in. $libdirexp/include
+    Standard headers installed in. $(expandprefix $libdir)/include
 EOF
 
 if $install_coqdev; then
 cat <<EOF
-    Coq development installed in.. $coqdevdirexp
+    Coq development installed in.. $(expandprefix $coqdevdir)
 EOF
 else
 cat <<EOF
-- 
cgit