merge and erase develop

@kaan.cimir so apparently some of the changes from Marina were merged into develop without anyone noticing. The same happened now in internal with Julia. Since we saw exactly zero use of develop except for 2 mismerges in the last half year, I'm deleting develop for safety reasons after this merge.