blob: 8ecb8fa4314745a21a630938da12b97b4f69d056 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
|
#! /bin/sh
#
# Necessary preparations/configurations for the reproduction pipeline.
#
# Original author:
# Your name <your@email.address>
# Contributing author(s):
# Copyright (C) YYYY, Your Name.
#
# This script is free software: you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation, either version 3 of the License, or
# (at your option) any later version.
#
# This script is distributed in the hope that it will be useful, but
# WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
# General Public License for more details.
#
# A copy of the GNU General Public License is available at
# <http://www.gnu.org/licenses/>.
# Location of the settings directory:
pdir=reproduce/config/pipeline
# If `LOCAL.mk' is already created, then ignore this step.
if [ -f $pdir/LOCAL.mk ]; then
echo
echo "$pdir/LOCAL.mk already exists."
echo "To change/correct the top-level directories, please remove/edit it manually."
echo
else
# Copy the base file to the desired output file.
if cp $pdir/LOCAL.mk.in $pdir/LOCAL.mk; then
# Tell the user to edit the directories.
while [ "$userread" != "y" -a "$userread" != "n" ]
do
echo
echo "------------------------------------"
echo "Reproduction pipeline local configuration"
echo "-----------------------------------------"
echo
echo "Local settings include things like top-level directories,"
echo "or processing steps (e.g., if you want a final PDF output)."
echo
echo "Pressing 'y' will open the local settings file in an editor"
echo "so you can modify the default values if you want. Each"
echo "variable is also thoroughly described in the comments (lines"
echo "starting with a '#') above it."
echo
read -p"Edit the default local configuration (y/n)? " userread
done
# Only continue if the user wants to edit the top level
# directories
if [ $userread = "y" ]; then
# Open a text editor to set the given directories
if emacs $pdir/LOCAL.mk; then junk=1
elif gedit $pdir/LOCAL.mk; then junk=1
elif vi $pdir/LOCAL.mk; then junk=1
else
echo
echo "No common text editor found on your system."
echo "Please set the values in '$pdir/LOCAL.mk' manually."
echo
fi
fi
echo
echo "This reproduction pipeline has been configured for this system."
echo "Please run the following command to start the pipeline:"
echo "(Replace '8' with the number of CPU threads available)"
echo
echo " make -j8"
echo
echo
echo "(you can always check/modify the default local settings"
echo " by editing this file: '$pdir/LOCAL.mk')"
echo
else
echo; echo "Couldn't create $pdir/LOCAL.mk"
fi
fi
|
