File: redirect.html.template

package info (click to toggle)
python-hypothesis 6.130.5-2
  • links: PTS, VCS
  • area: main
  • in suites: trixie
  • size: 14,884 kB
  • sloc: python: 59,532; ruby: 1,107; sh: 251; makefile: 45
file content (38 lines) | stat: -rw-r--r-- 1,924 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
<!DOCTYPE html>
<html>
  <head>
    <noscript>
      <meta http-equiv="refresh" content="0; url=${to_uri}" />
    </noscript>
    <script>
      var target = "${to_uri}";

      var manualRedirects = {
        "details.html#thread-safety-policy": "supported.html#thread-safety-policy",
        "details.html#hypothesis.given": "reference/api.html#hypothesis.given",
        "details.html#targeted-example-generation": "reference/api.html#targeted-property-based-testing",
        "details.html#custom-function-execution": "reference/api.html#custom-function-execution",
        // TODO_DOCS when we figure out a home for this page
        // "details.html#type-annotations-in-hypothesis": ""
        "details.html#the-hypothesis-pytest-plugin": "reference/integrations.html#the-hypothesis-pytest-plugin",
        "details.html#use-with-external-fuzzers": "reference/api.html#use-with-external-fuzzers",
        "details.html#making-assumptions": "reference/api.html#hypothesis.assume",
        "details.html#hypothesis.event": "reference/api.html#hypothesis.event",
        "details.html#hypothesis.assume": "reference/api.html#hypothesis.assume",
        "details.html#hypothesis.given": "reference/api.html#hypothesis.given",
        "details.html#hypothesis.target": "reference/api.html#hypothesis.target",
        "details.html#hypothesis.register_random": "reference/strategies.html#hypothesis.register_random",
        "details.html#hypothesis.strategies.SearchStrategy": "reference/strategies.html#hypothesis.strategies.SearchStrategy",
      };
      var redirect = manualRedirects[window.location.pathname.split('/').pop() + window.location.hash];

      if (redirect) {
        window.location.replace(redirect);
      } else if (window.location.hash) {
        window.location.replace(target + window.location.hash);
      } else {
        window.location.replace(target);
      }
    </script>
  </head>
</html>