Le 26/05/2019 à 16:47, Antonio Ospite a écrit :
> From: Antonio Ospite
>
> Since commit 79d77bcd36 (configure: Remove --source-path option,
> 2019-04-29) source_path cannot be overridden anymore, move it out of the
> "default parameters" block since the word "default" may suggest that the
> value
From: Antonio Ospite
Since commit 79d77bcd36 (configure: Remove --source-path option,
2019-04-29) source_path cannot be overridden anymore, move it out of the
"default parameters" block since the word "default" may suggest that the
value can change, while in fact it does not.
While at it, only s
