diff --git a/.aliases b/.aliases index 69449c4..b21b1eb 100644 --- a/.aliases +++ b/.aliases @@ -85,7 +85,7 @@ alias remove="sudo apt-get remove " # To use this - Ensure all git server SSH are in ~/.ssh alias git_signin='(for i in ~/.ssh/{*github*,*bitbucket*,*gitea*,*gitlab*}; do ssh-add -k $i; done; ) && (echo; echo Identities added successfully)' git_push_all_changes(){ - git commit -am "${1}" && git push + git add . && git commit -am "${1}" && git push } # Add ~/.local/bin to PATH diff --git a/.config/Code/User/settings.json b/.config/Code/User/settings.json index 1b63ef2..d9754c8 100644 --- a/.config/Code/User/settings.json +++ b/.config/Code/User/settings.json @@ -1,4 +1,4 @@ -{ + { // Global "update.mode": "manual", "workbench.settings.editor": "json", @@ -87,6 +87,7 @@ "GOPATH", "Jython", "Kumar", + "Monomorphization", "OOP", "Odisha", "Pratik", @@ -105,6 +106,7 @@ "destructure", "elif", "mkdir", + "monomorphized", "pratiktri", "ptr", "pylint",