[robocop] tag v1.0.0 updated (e9b7c1c -> f7d751d)

[Admin]

This is an automated email from the git hooks/post-receive script.

grothoff pushed a change to tag v1.0.0
in repository robocop.

*** WARNING: tag v1.0.0 was modified! ***

    from e9b7c1c  (commit)
      to f7d751d  (commit)
    from e9b7c1c  add -h/-v command-line options
     add f7d751d  add minimal GNU-style build system

No new revisions were added by this update.

Summary of changes:
 Makefile.in | 15 +++++++++++++
 bootstrap   |  4 ++++
 configure   | 72 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 91 insertions(+)
 create mode 100644 Makefile.in
 create mode 100755 bootstrap
 create mode 100755 configure

diff --git a/Makefile.in b/Makefile.in
new file mode 100644
index 0000000..472847a
--- /dev/null
+++ b/Makefile.in
@@ -0,0 +1,15 @@
+PREFIX=%PREFIX%
+install:
+       cargo install --path . --root $(PREFIX)
+       cp robocop-ch-to-json $(PREFIX)/bin
+       cp robocop-json-postprocess $(PREFIX)/bin
+        rm -rf debian/tmp/usr/.crates*
+
+test:
+       RUST_BACKTRACE=full cargo run --profile dev --bin instrumentation -- 
offline
+
+check:
+       cargo check
+
+msrv:
+       cargo msrv --min 1.70.0
diff --git a/bootstrap b/bootstrap
new file mode 100755
index 0000000..695f2d7
--- /dev/null
+++ b/bootstrap
@@ -0,0 +1,4 @@
+#!/bin/sh
+# This file is in the public domain.
+chmod +x configure
+exit 0
diff --git a/configure b/configure
new file mode 100755
index 0000000..4717758
--- /dev/null
+++ b/configure
@@ -0,0 +1,72 @@
+#!/bin/sh
+# This file is in the public domain.
+# Minimal GNU-style configure script
+# Default values
+prefix="/usr/local"
+
+# Function to display help
+show_help() {
+    cat << EOF
+Usage: $0 [OPTION]...
+
+Configuration options:
+  --help              display this help and exit
+  --prefix=PREFIX     install files under this PREFIX
+                      [default: /usr/local]
+
+Report bugs to https://bugs.taler.net/
+EOF
+}
+
+# Parse command line arguments
+while test $# -gt 0; do
+    case "$1" in
+        --help | -h)
+            show_help
+            exit 0
+            ;;
+        --prefix=*)
+            prefix=$(echo "$1" | sed 's/--prefix=//')
+            ;;
+        --prefix)
+            shift
+            if test $# -eq 0; then
+                echo "configure: error: option '--prefix' requires an 
argument" >&2
+                exit 1
+            fi
+            prefix="$1"
+            ;;
+        *)
+            echo "configure: error: unrecognized option: '$1'" >&2
+            echo "Try '$0 --help' for more information." >&2
+            exit 1
+            ;;
+    esac
+    shift
+done
+
+# Check if Makefile.in exists
+if test ! -f Makefile.in; then
+    echo "configure: error: Makefile.in not found" >&2
+    exit 1
+fi
+
+# Generate Makefile from Makefile.in
+echo "configuring with prefix: $prefix"
+echo "generating Makefile..."
+
+# Use sed to replace %PREFIX% with the actual prefix value
+sed "s|%PREFIX%|$prefix|g" Makefile.in > Makefile
+
+if test $? -eq 0;
+then
+    echo "configure: Makefile created successfully"
+    echo ""
+    echo "Configuration summary:"
+    echo "  Install prefix: $prefix"
+    echo ""
+    echo "Now run 'make' to build the project."
+else
+    echo "configure: error: failed to create Makefile" >&2
+    exit 1
+fi

-- 
To stop receiving notification emails like this one, please contact
gnunet@gnunet.org.