Merge branch 'main' into release
This commit is contained in:
commit
8a7cbc484e
4
justfile
4
justfile
|
@ -29,10 +29,10 @@ release:
|
|||
echo {{ if git_status == "" {"git status ok"} else {error("please commit changes first")} }}
|
||||
just build
|
||||
git checkout release
|
||||
git merge {{from_branch}}
|
||||
git merge main
|
||||
-git commit -am "release build"
|
||||
git checkout main
|
||||
git push
|
||||
git checkout {{from_branch}}
|
||||
|
||||
# serve the pkg directory
|
||||
serve:
|
||||
|
|
|
@ -96,7 +96,7 @@ function bundle_keys () {
|
|||
}
|
||||
|
||||
function start_io_polling () {
|
||||
io_interval_id = setInterval(io_poller, 100)
|
||||
io_interval_id = setInterval(io_poller, 10)
|
||||
}
|
||||
|
||||
// runs a ludus script; does not return the result
|
||||
|
|
Loading…
Reference in New Issue
Block a user