diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2000-04-28 17:53:53 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2000-04-28 17:53:53 +0000 |
commit | 7049d068a894b82ba809a7ce49daf411d7d2dce5 (patch) | |
tree | a7f0ed5a518c5b21b9aa6c0ffa453e008c106df9 /etc/cvs-tips.txt | |
parent | e80b0bb50b45b89c520754271096964047481209 (diff) |
Note about conflict in merging
Diffstat (limited to 'etc/cvs-tips.txt')
-rw-r--r-- | etc/cvs-tips.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/etc/cvs-tips.txt b/etc/cvs-tips.txt index a529b398..0678b1cd 100644 --- a/etc/cvs-tips.txt +++ b/etc/cvs-tips.txt @@ -27,5 +27,7 @@ Then perhaps merge in branch changes into main stream: cd projects/proofgen/ProofGeneral cvs update -jRelease-3-1-branch +NB: this merging will always create conficts with +$Id$ tags in source. (Is there a way to avoid this?)
\ No newline at end of file |