git merge strange result

Hello!

Below is a script that reproduce what a coleague of mine found.
Seems that if in a branch we have a commit that is cherry-picked be 
master, than revert that commit in branch and merge branch in master, the 
revert is ignored. Is it normal?

Thank you very much!

#!/bin/bash

set -e

rm -rf buba1
mkdir buba1
cd buba1

git init
echo -e "aaa\nbbb\nccc" > file1
git add file1
git commit -m "c1"

echo "Create branch b1..."
git branch b1
echo

echo "Create a bad fix..."
sed --in-place -e 's/bbb/bad line/' file1
git add file1
git commit -m "bad commit"
cat file1
echo

echo "Cherry pick on b1..."
git checkout b1
git cherry-pick -x master
echo

echo "Reverting on b1"
git revert --no-edit b1
echo

echo "Switch to master"
git checkout master
echo

echo "merge-base is `git merge-base --all master b1 | git name-rev --stdin`"
echo

echo "diff between master and b1..."
git diff master b1
echo

echo "Merge b1 in master"
git merge --verbose --log b1

if [ "`grep bad file1`" = "" ]; then
 	echo "good!"
else
 	echo "bad!"
fi
# it should prind "good"

--
Catalin(ux) M. BOIE
http://kernel.embedromix.ro/