aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/cvs-tips.txt
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-28 17:53:53 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2000-04-28 17:53:53 +0000
commit7049d068a894b82ba809a7ce49daf411d7d2dce5 (patch)
treea7f0ed5a518c5b21b9aa6c0ffa453e008c106df9 /etc/cvs-tips.txt
parente80b0bb50b45b89c520754271096964047481209 (diff)
Note about conflict in merging
Diffstat (limited to 'etc/cvs-tips.txt')
-rw-r--r--etc/cvs-tips.txt2
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