Rename file

_web_server/server/firejailed.sh

@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-
-exe=$(basename $0)
-
-exec firejail --noprofile --quiet \
-     --rlimit-cpu=1               \
-     --rlimit-as=100m             \
-     --rlimit-fsize=1m            \
-     "$exe" "$@"

_web_server/server/iverilog

@@ -1 +1 @@
-./firejailed.sh
+run-restricted

_web_server/server/run-restricted

@@ -0,0 +1,14 @@
+#!/usr/bin/env bash
+
+exe=$(basename $0)
+
+if [ -z "$DONOTUSEFIREJAIL" ]; then
+    exec firejail              \
+         --quiet --noprofile   \
+         --rlimit-cpu=5        \
+         --rlimit-as=250m      \
+         --rlimit-fsize=250k   \
+         "$exe" "$@"
+else
+    exec timeout -v -s INT 5 "$exe" "$@"
+fi

_web_server/server/vvp

@@ -1 +1 @@
-./firejailed.sh
+run-restricted