UPDATE: GIT is actually smart enough it seems, but it is taking many hours for it to merge everything correctly. I wish I could upgrade that server...
Okay. Whew! Still, lesson learned: git pull BEFORE pushing. Actually, git pull BEFORE patching too.
BTW, my previous link includes a patch for tdewebdev. David, please test!
Darrell