From c47b83bc6a72563f3aa28e19968f4cb48eb8b72d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 21 Feb 2022 14:54:09 +0100
Subject: [PATCH] [Dune] dune file generator for plugins

---
 bin/init-plugin.sh | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100755 bin/init-plugin.sh

diff --git a/bin/init-plugin.sh b/bin/init-plugin.sh
new file mode 100755
index 00000000000..382c06b86c7
--- /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
-- 
GitLab