From 9db03020a7004e1b7de1e0a8292f1b46f5ea3602 Mon Sep 17 00:00:00 2001
From: Philippe Heim <philippe.heim@cispa.de>
Date: Mon, 8 Apr 2024 12:14:26 +0200
Subject: [PATCH] small fixes

---
 .dockerignore       | 2 +-
 benchmarking/run.sh | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.dockerignore b/.dockerignore
index 7bef3c5..83d2a3b 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -25,4 +25,4 @@
 **/*.pdf
 **/*.tar
 docker-output
-README.md
\ No newline at end of file
+rpg-stela-docker.tar
diff --git a/benchmarking/run.sh b/benchmarking/run.sh
index c46c265..e80b159 100644
--- a/benchmarking/run.sh
+++ b/benchmarking/run.sh
@@ -87,7 +87,7 @@ execute_file() {
     shortname=$(basename "$filename" | sed 's/\.[^.]*$//')
 
     ### details about the benchmark ###
-    if grep -q "Real" <<< "$content"; then
+    if grep -q "Real" < "$filename"; then
         domain="R"
     else
         domain="Z"
-- 
GitLab