Bug#903428: deduplicating jquery/

[Samuel Thibault]

Emmanuel Bourg, le lun. 07 janv. 2019 22:25:35 +0100, a ecrit:
> Le 07/01/2019 à 21:13, Nicholas D Steeves a écrit :
> > Do you have any suggestions for working with the following?: (please
> > reply to -devel)
> 
> We've discussed this topic in #903428 and the consensus is roughly that
> it's a waste of time and we would rather drop the mostly unused javadoc
> packages than implementing this.

I'd rather cripple the documentation a bit than removing it :)

Could jh_build perhaps just drop the embedded jquery copy to just avoid
the issue? AFAIK, jquery is only used to implement the "search" feature,
which can sometimes be convenient, but can be done by users with greps &
such.

Samuel