#!/bin/sh # # High-level script to manage the project. # Run `./project --help' for a description of how to use it. # # Copyright (C) 2019-2020 Mohammad Akhlaghi # # This program 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 program 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. # # You should have received a copy of the GNU General Public License # along with this program. If not, see . # Basic settings # -------------- # Stop the script if there are any errors. set -e # Default option values jobs=0 # 0 is for the default for the `configure.sh' script. group= debug= host_cc=0 operation= build_dir= input_dir= check_config= make_targets= software_dir= clean_texdir=0 prepare_redo=0 all_highlevel=0 existing_conf=0 scriptname="./project" minmapsize=10000000000 # Parse the options # ----------------- # # Separate command-line arguments from options. Then put the option value # into the respective variable. # # Each option has two lines because we want to process both these formats: # `--name=value' and `--name value'. The former (with `=') is a single # command-line argument, so we just need to shift the counter by one. The # latter (without `=') is two arguments, so we'll need two shifts. # # Note on the case strings: for every option, we need three lines: one when # the option name and value are separate. Another when there is an equal # between them, and finally one where the value is immediately after the # short-format. This exact order is important. Otherwise, there will be a # conflict between them. print_help() { # Print the output. cat < /dev/null > /dev/null; then coloropt="--color=auto" elif ls -G 2> /dev/null > /dev/null; then coloropt="-G" else coloropt="" fi # Print a notice to let the user know what is happening. cat < /dev/null" &> /dev/null; then echo "$scriptname: '$group' is not a usable group name on this system."; echo "(TIP: you can use the 'groups' command to see your groups)" exit 1 fi # Set the group option for running Make. gopt="reproducible_paper_group_name=$group" fi # Error when configuration isn't run configuration_necessary() { cat <