diff options
| -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 |