Git develop branch.

[jan i]

Hi.

maybe its just me, but should we not delete "develop" on the server ?

rgds
jan i.