From 23eef76da18d4dd8043f638309297a455da6f90d Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 7 Nov 2024 07:39:58 +0000
Subject: [PATCH] Update informal.lean

---
 scripts/MetaPrograms/informal.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/scripts/MetaPrograms/informal.lean b/scripts/MetaPrograms/informal.lean
index b7f1bcd..a65aecf 100644
--- a/scripts/MetaPrograms/informal.lean
+++ b/scripts/MetaPrograms/informal.lean
@@ -16,6 +16,7 @@ import ImportGraph.RequiredModules
 To make the dot file for the dependency graph run:
 - lake exe informal mkDot
 - dot -Tsvg -o ./Docs/graph.svg ./Docs/InformalDot.dot
+- or dot -Tpng  -Gdpi=300 -o ./Docs/graph.png ./Docs/InformalDot.dot
 -/
 
 open Lean System Meta