* Mosè Giordano (2013-07-19) writes: > 2013/7/19 Ralf Angeli <[email protected]>: >> >> Here are a few points that caught my eye: >> >> -COMMITTER="David Kastrup <[email protected]>" >> +COMMITTER="`git config user.name` \<`git config user.email`\>" >> >> Those two commands return nothing if I execute them on the command line. >> I'm a git novice, so I might have misconfigured it. But at least `git >> pull' works. (c: > > If those `git config' commands return nothing then you can pass > `COMMITTER' values as a command line argument, as usual. To setup > those keys run > git config --global user.name "John Doe" > git config --global user.email [email protected] > However, probably it's safer to obtain keys values with `--get' option.
Hm, git config --get user.name did not get the user name. I'll look into this more closely when I have to make my commit with git which I expect to fail. >> + git tag release_`echo $(TAG) | sed -e 's/[.]/_/g'` >> + rm ChangeLog.old >> >> If you want to delete the old ChangeLog file is probably a matter of >> taste. When something goes wrong you'd have to edit the new ChangeLog >> file and cannot just move the old one back in place. > > Ok, I'll remove the `rm', but you can bring back the previous > ChangeLog with `git checkout HEAD^ ChangeLog'. As I wrote, this is a matter of taste. If you like the change, keep it. I don't object to it. > The attached patch should fix the problems you pointed out. Great, thanks! -- Ralf _______________________________________________ auctex-devel mailing list [email protected] https://lists.gnu.org/mailman/listinfo/auctex-devel
