diff --git a/bin/init-plugin.sh b/bin/init-plugin.sh new file mode 100755 index 0000000000000000000000000000000000000000..382c06b86c71ed1d002b34b0b73c94001a32fd72 --- /dev/null +++ b/bin/init-plugin.sh @@ -0,0 +1,36 @@ +#! /usr/bin/env bash + +if [[ $# != 1 && $# != 2 ]]; then + echo "Usage: $0 <plugin-name> [<directory>]" + exit 2 +fi +if [[ $# == 1 ]]; then + directory="." +else + directory=$2 +fi + +if [[ ! -d $directory ]]; then + echo "'$directory': not such file or directory" + exit 17 +fi + +echo "Target directory is '$directory'" + +dune_file=$directory/dune + +if [[ -f $dune_file ]]; then + echo "'$dune_file' file already exists." + exit 17 +fi + +cat > $dune_file <<EOF +( library + (name $1) + (public_name frama-c-$1.core) + (flags -open Frama_c_kernel :standard) + (libraries frama-c.kernel) +) + +(plugin (optional) (name $1) (libraries frama-c-$1.core) (site (frama-c plugins))) +EOF