From c0eaeb249c8fd246f3a56f18f61e417c277f43c1 Mon Sep 17 00:00:00 2001
From: Arnaud Giersch <arnaud.giersch@iut-bm.univ-fcomte.fr>
Date: Wed, 7 Mar 2012 12:13:30 +0100
Subject: [PATCH 1/1] make_params: PREFIX can be set from 2nd parameter on
command line.
---
Experimentations/make_params | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Experimentations/make_params b/Experimentations/make_params
index dd7e201..2d5c26b 100755
--- a/Experimentations/make_params
+++ b/Experimentations/make_params
@@ -3,7 +3,7 @@
set -e
TEMPLATE=${1:-"ag_parameters"}
-PREFIX=param
+PREFIX=${2:-"param"}
log() {
echo "-#- $@" >&2
--
2.39.5