Merge jt

I am a simple man. I see double, I upvote (where is the upvote button for commits?!).

I dont think we use double anywhere except the automata generators (where integer suffices) but thank youu :-)

merged