<!--
- Translation of GIT committish: 9d074d78d7c25852afa87005e21c118630f4f83b
+ Translation of GIT committish: 1df9fc42197a6b2931f448cfba717527aead5e5a
When revising a translation, copy the HEAD committish of the
version that you are working on. See TRANSLATION for details.
-->
-<!--
-we depend on an external entity here, which we cannot control. Suppose
-we go from 2.15.x to 2.17.x and put the documentation under "v2.17".
-For some time, Google won't have the new location in its index, so the
-search would get nothing. It would be better to keep "v2.15" in the
-search for a while and have a redirection from "v2.15" to "v2.17".
--->
<form action="http://google.com/search"
method="get"
name="search"