From 457574615bf4842709affa7311e1f81839bfa7dc Mon Sep 17 00:00:00 2001 From: Ivan Tkatchev Date: Tue, 22 Mar 2022 21:40:40 +0300 Subject: [PATCH] Add -p command line option. --- docs/website/index.html | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/docs/website/index.html b/docs/website/index.html index bb1d00a..ad924ef 100644 --- a/docs/website/index.html +++ b/docs/website/index.html @@ -120,6 +120,13 @@

History

+
2022-03-22
+
Version 9.1 released. Changes: +
    +
  • Added the -p command line option for setting the prelude.
  • +
+
+
2022-02-16
Version 9.0 released. Changes: