From 88bc7f1209668aa64b2f110121f6f4a2506b9d0c Mon Sep 17 00:00:00 2001
From: johannst <johannst@users.noreply.github.com>
Date: Thu, 7 Jul 2022 20:23:13 +0000
Subject: deploy: 8018375d79d74f2911c335337722a719cf87c72e

---
 tools/dot.html | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tools/dot.html')

diff --git a/tools/dot.html b/tools/dot.html
index 05f652d..b3164d9 100644
--- a/tools/dot.html
+++ b/tools/dot.html
@@ -153,7 +153,8 @@
                 <div id="content" class="content">
                     <main>
                         <h1><a class="header" href="#dot1" id="dot1">dot(1)</a></h1>
-<p>Example <code>dot</code> file to copy &amp; paste from.</p>
+<p><a href="https://edotor.net/">Online playground</a></p>
+<h2><a class="header" href="#example-dot-file-to-copy--paste-from" id="example-dot-file-to-copy--paste-from">Example <code>dot</code> file to copy &amp; paste from.</a></h2>
 <p>Can be rendered to <code>svg</code> with the following command.</p>
 <pre><code class="language-bash">dot -T svg -o g.svg g.dot
 </code></pre>
-- 
cgit v1.2.3