<pre style='margin:0'>
Landon Fuller (landonf) pushed a commit to branch master
in repository macports-ports.

</pre>
<p><a href="https://github.com/macports/macports-ports/commit/9fab1cb482a95d82830f8b7516ef4d5069dbffe7">https://github.com/macports/macports-ports/commit/9fab1cb482a95d82830f8b7516ef4d5069dbffe7</a></p>
<pre style="white-space: pre; background: #F8F8F8"><span style='display:block; white-space:pre;color:#808000;'>commit 9fab1cb482a95d82830f8b7516ef4d5069dbffe7
</span>Author: Landon Fuller <landonf@macports.org>
AuthorDate: Mon Jan 18 19:00:29 2021 -0700

<span style='display:block; white-space:pre;color:#404040;'>    kremlin-devel: do not pass --lax when driving F* for Kremlin codegen
</span><span style='display:block; white-space:pre;color:#404040;'>    
</span><span style='display:block; white-space:pre;color:#404040;'>    Without this, the default krml behavior (when using legacy support
</span><span style='display:block; white-space:pre;color:#404040;'>    for driving F* via KreMLin) may result in (an attempt) to write
</span><span style='display:block; white-space:pre;color:#404040;'>    *.checked.lax files to ${prefix}.
</span>---
 lang/fstar/Portfile                                      |  3 ++-
 lang/fstar/files/kremlin-devel/patch-fstar-driver-no-lax | 12 ++++++++++++
 2 files changed, 14 insertions(+), 1 deletion(-)

<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/Portfile b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;color:#808080;'>index f7273c3a35d..85ed4e0892a 100644
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>--- a/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/Portfile
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -228,7 +228,7 @@ subport kremlin {
</span> subport kremlin-devel {
     github.setup        ${github.author} ${fstar.project} 18a6351f033ead59faa9c70d4cafa8be76c43adb
     version             ${fstar.version}-[string range ${github.version} 0 6]
<span style='display:block; white-space:pre;background:#ffe0e0;'>-    revision            0
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+    revision            1
</span> 
     checksums           rmd160  ec2932944a1a875a84195ab125b5a5084af882ad \
                         sha256  fe29545aac1548a428e894fbe19c18ac2e7f68dfe44b01d6a05666fbc0ba99f6 \
<span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -237,6 +237,7 @@ subport kremlin-devel {
</span>     patchfiles-append   kremlin-devel/patch-clang-driver-options \
                         kremlin-devel/patch-fix-make-command \
                         kremlin-devel/patch-fstar-discover-path \
<span style='display:block; white-space:pre;background:#e0ffe0;'>+                        kremlin-devel/patch-fstar-driver-no-lax \
</span>                         kremlin-devel/patch-test_system_system.h
 
     depends_lib-append  port:ocaml-sedlex
<span style='display:block; white-space:pre;color:#808080;'>diff --git a/lang/fstar/files/kremlin-devel/patch-fstar-driver-no-lax b/lang/fstar/files/kremlin-devel/patch-fstar-driver-no-lax
</span>new file mode 100644
<span style='display:block; white-space:pre;color:#808080;'>index 00000000000..18e5bf68347
</span><span style='display:block; white-space:pre;background:#ffe0e0;'>--- /dev/null
</span><span style='display:block; white-space:pre;background:#e0e0ff;'>+++ b/lang/fstar/files/kremlin-devel/patch-fstar-driver-no-lax
</span><span style='display:block; white-space:pre;background:#e0e0e0;'>@@ -0,0 +1,12 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+--- src/Driver.ml.orig     2021-01-18 16:45:56.000000000 -0700
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++++ src/Driver.ml  2021-01-18 16:46:28.000000000 -0700
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+@@ -349,8 +349,7 @@
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+   else
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     let args =
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+       "--odir" :: !Options.tmpdir ::
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-      "--codegen" :: "Kremlin" ::
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+-      "--lax" :: args
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>++      "--codegen" :: "Kremlin" :: args
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     in
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     flush stdout;
</span><span style='display:block; white-space:pre;background:#e0ffe0;'>+     mk_tmpdir_if ();
</span></pre><pre style='margin:0'>

</pre>