summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorErich Eckner <git@eckner.net>2018-06-26 09:12:09 +0200
committerErich Eckner <git@eckner.net>2018-06-26 09:12:09 +0200
commit4eb3face7bd2fc2e3fd62139fe7e110ddba499a9 (patch)
treea93e9e2d7b796180db28016e55d5642e2fe0d4a2
parent31d142f5ac9dbbca62534b636ebdc6229cfeb00b (diff)
downloadwebsite-4eb3face7bd2fc2e3fd62139fe7e110ddba499a9.tar.xz
"dot" -> "timeout 30 dot"
-rw-r--r--buildmaster/build-list-links.php2
-rw-r--r--buildmaster/deletion-links.php2
-rw-r--r--buildmaster/dependencies.php2
-rw-r--r--buildmaster/todos.php2
4 files changed, 4 insertions, 4 deletions
diff --git a/buildmaster/build-list-links.php b/buildmaster/build-list-links.php
index 6604825..3d4badf 100644
--- a/buildmaster/build-list-links.php
+++ b/buildmaster/build-list-links.php
@@ -224,7 +224,7 @@ if (isset($_GET["raw"])) {
header ("Content-type: image/png");
passthru(
- "dot -Tpng -o/dev/stdout " . $input_file
+ "timeout 30 dot -Tpng -o/dev/stdout " . $input_file
);
unlink($input_file);
diff --git a/buildmaster/deletion-links.php b/buildmaster/deletion-links.php
index 6b00c65..f3a0aef 100644
--- a/buildmaster/deletion-links.php
+++ b/buildmaster/deletion-links.php
@@ -226,5 +226,5 @@ passthru(
"}\n"
) . "' | " .
"base64 -d | " .
- "dot -Tpng -o/dev/stdout /dev/stdin"
+ "timeout 30 dot -Tpng -o/dev/stdout /dev/stdin"
);
diff --git a/buildmaster/dependencies.php b/buildmaster/dependencies.php
index 8eb4dc4..fb168a1 100644
--- a/buildmaster/dependencies.php
+++ b/buildmaster/dependencies.php
@@ -156,7 +156,7 @@ $edges = str_replace("\$","\\\$",$edges);
header ("Content-type: image/png");
passthru(
- "dot -Tpng -o/dev/stdout /dev/stdin <<EOF\n" .
+ "timeout 30 dot -Tpng -o/dev/stdout /dev/stdin <<EOF\n" .
"digraph dependencies {\n" .
"rankdir=LR;\n" .
"fontname=dejavu;\n" .
diff --git a/buildmaster/todos.php b/buildmaster/todos.php
index b175350..e3d7319 100644
--- a/buildmaster/todos.php
+++ b/buildmaster/todos.php
@@ -59,7 +59,7 @@ if (isset($_GET["graph"])) {
"}\n"
) . "\" | " .
"base64 -d | " .
- "dot -Tpng -o/dev/stdout /dev/stdin"
+ "timeout 30 dot -Tpng -o/dev/stdout /dev/stdin"
);
} else { // isset($_GET["graph"])