why does RAND_add() take "randomness" as a "double"?

[Salz, Rich]

>    If it's a sarcasm, I'm missing the point.
  
I was't being sarcastic, I was trying to show that the team, recently, still liked the use of floating point.

>    There are use cases when one wants to mix/add extra randomness from, e.g., an external source (that, for whatever reasons, is trusted more than what's provided by the system).
 
Then just set it to 1.0 and be done with it.