diff --git a/3rdparty/mmu_man/scripts/dev-perso b/3rdparty/mmu_man/scripts/dev-perso index 4d6f497c2a..b5a786d252 100755 --- a/3rdparty/mmu_man/scripts/dev-perso +++ b/3rdparty/mmu_man/scripts/dev-perso @@ -131,9 +131,15 @@ dev() { ;; esac + # check for a TODO list + for f in TODO TODO.org; do + test -e "$f" && grep '^* ' "$f" | grep --color=always ' TODO ' | head -5 && break + done + DEVUPCMD="" # source the specific profile file + # (which will likely cd to the checkout directory) test -f .profile && . .profile # if no editor defined, set one