Yesterday I pushed a fix from Dan upstream, and this morning the fix wasn't there anymore. Some unrelated fix was merged in the meantime.
I only realized this because I was updating my personal origin and git wouldn't allow me to push the non-fast-forward branch, so in a sense I could detect it because of how our workflow works (good). I have no idea of how it happened, but I guess it won't hurt to remind that we should never push with --force, at least not without warning the whole list. I now cherry-picked and fixed master by re-pushing the missing patch, so nothing bad happening :-) Sanne _______________________________________________ infinispan-dev mailing list [email protected] https://lists.jboss.org/mailman/listinfo/infinispan-dev
