Compare commits
2 commits
cfa995180e
...
2a10b068c6
Author | SHA1 | Date | |
---|---|---|---|
2a10b068c6 | |||
b6ce349681 |
2 changed files with 3 additions and 0 deletions
|
@ -2,5 +2,6 @@ using OhMyREPL
|
||||||
using Pluto
|
using Pluto
|
||||||
using Symbolics
|
using Symbolics
|
||||||
using Unitful
|
using Unitful
|
||||||
|
using Nemo
|
||||||
τ = 2*π
|
τ = 2*π
|
||||||
pluto_custom() = Pluto.run(;port=8080, host="0.0.0.0", auto_reload_from_file=true, require_secret_for_access=false, warn_about_untrusted_code=false)
|
pluto_custom() = Pluto.run(;port=8080, host="0.0.0.0", auto_reload_from_file=true, require_secret_for_access=false, warn_about_untrusted_code=false)
|
||||||
|
|
|
@ -23,6 +23,8 @@ fi
|
||||||
# Avoiding copy pasting this over and over
|
# Avoiding copy pasting this over and over
|
||||||
g() { git -C "$REPO" "$@"; }
|
g() { git -C "$REPO" "$@"; }
|
||||||
|
|
||||||
|
REPOS_TO_UPDATE="${REPOS_TO_UPDATE:-}"
|
||||||
|
|
||||||
# path_append from https://superuser.com/questions/39751/add-directory-to-path-if-its-not-already-there
|
# path_append from https://superuser.com/questions/39751/add-directory-to-path-if-its-not-already-there
|
||||||
# checks if a path is already in the PATH and if it exists
|
# checks if a path is already in the PATH and if it exists
|
||||||
path_append() {
|
path_append() {
|
||||||
|
|
Loading…
Add table
Reference in a new issue