Provide the source file name to the JS in readthedocs theme

readthedocs.org needs the file name in order to identify the correct source
file to link to the same file in other versions of the same documentation or
to the source on GitHub.

Related readthedocs/readthedocs.org#1480

Author: gregmuellegger

mkdocs/themes/readthedocs/base.html

@@ -26,7 +26,7 @@
   {% if current_page %}
   <script>
     // Current page data
-    var mkdocs_page_name = "{{ page_title }}";
+    var mkdocs_page_name = "{{ current_page.input_path[:current_page.input_path.rfind('.')] }}";
     var mkdocs_page_url = "{{ current_page.abs_url }}";
   </script>
   {% endif %}