Git: Push local file to a different file name in a remote repository

Question

I'm working on a specialized standalone server for imageboards, and have the local git repository folder as my development/testing folder. Is it possible to push a local file to the repository with a different name? For example, index.html.remote (on the local repo) to index.html (remote repo), since gochan uses template files to generate html pages. I could just create index.html as an landing page for first time installation, push that, and then just replace that with a template-generated version and never push it again, but that seems a bit messy.

Answer 1

But having it as just index.html when a user first downloads it would look better than index.html.remote, wouldn't it?

You can achieve that. Simply version a:

• index.html.template
• a script which generates the right index.html (not versioned, private)
• a .gitattributes file in which you declare that content filter driver called here "smudge" (a script which runs on git checkout)

(picture from chapter "git Attributes" of the Git book)

echo 'index.html.template tpl' >> .gitattributes
git config --global filter.tpl.smudge yourScript

That way, you don't have to push different files to different remotes.
You manage only one file (a template file), and your script generates the right content depending on its execution environment.