lake scripts with args

Stream: lean4

[Arthur Paulino]

I'm trying to run a lake script with arguments. My script starts with

script kcompile (args) do
  ...

When I hover args it indeed says List String, but when I call lake run kcompile arg1 arg2 it says:
error: unexpected arguments: arg1 arg2
Is this feature still WIP?

[Henrik Böving]

maybe it expects you do do lake run kcompile -- arg1 arg2 ?

[Arthur Paulino]

Ah, that works! But it's different form what's said here

[Henrik Böving]

@Mac is this intended?

[Mac]

lake run was upgraded into lake script run which has a slightly different syntax (but that change had yet to be merged into the Lake of Lean).