Compare commits
No commits in common. "2a10b068c62439555d2352116f7a812227081532" and "cfa995180eb242c34b7d59b84efc4d0f4e9d9a2d" have entirely different histories.
2a10b068c6
...
cfa995180e
2 changed files with 0 additions and 3 deletions
|
@ -2,6 +2,5 @@ using OhMyREPL
|
|||
using Pluto
|
||||
using Symbolics
|
||||
using Unitful
|
||||
using Nemo
|
||||
τ = 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)
|
||||
|
|
|
@ -23,8 +23,6 @@ fi
|
|||
# Avoiding copy pasting this over and over
|
||||
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
|
||||
# checks if a path is already in the PATH and if it exists
|
||||
path_append() {
|
||||
|
|
Loading…
Add table
Reference in a new issue