Add -p command line option.

ivan-tkatchev · Mar 22, 2022 · 4575746 · 4575746
1 parent d1f0306
commit 4575746
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/docs/website/index.html b/docs/website/index.html
@@ -120,6 +120,13 @@ <h1>History</h1>
 
     <dl>
 
+        <dt>2022-03-22</dt>
+        <dd>Version 9.1 released. Changes:
+            <ul>
+                <li>Added the <code>-p</code> command line option for setting the prelude.</li>
+            </ul>
+        </dd>
+
         <dt>2022-02-16</dt>
         <dd>Version 9.0 released. Changes:
             <ul>