View git-rename-branch.sh
# 1. rename local branch | |
git branch -m new_branch | |
# 2. delete old branch from remote | |
git push origin :old_branch | |
# 3. push & create new branch to upstream | |
git push --set-upstream origin new_branch |
View git-rename-branch.sh
# 1. rename local branch | |
git branch -m new_branch | |
# 2. delete old branch from remote | |
git push origin :old_branch | |
# 3. push & create new branch to upstream | |
git push --set-upstream origin new_branch |
View github-editor-textarea-enlarger.css
/* | |
. solution already provided by CodeMirror (https://codemirror.net/demo/resize.html#). | |
. to implement it, we must create an browser app in order to load it each time a gist editor will be opened | |
. in case of chrome, app already created, you can use it and follow manual for more details | |
(https://github.com/haythamdouaihy/github-editor-textarea-enlarger-chrome-ext) | |
*/ | |
.CodeMirror { | |
border: 1px solid #eee; | |
height: auto; |
View update-git-repos-reset-hard.sh
#!/bin/bash | |
# store the current dir | |
CUR_DIR=$(pwd) | |
# retrieve base repo parameter | |
# 1st param: alias of the remote repo URL (example: origin) | |
# 2nd param: remote branch name (example: master) | |
BASE_REPO="$1"/"$2" |
View gist:682d7c808933bc7704d0
-- query that returns duplicate colum value | |
select | |
count(<duplicated_column_name>), | |
<duplicated_column_name>, | |
<other> | |
from | |
<table_name> | |
group by | |
<duplicated_column_name> | |
HAVING |