debian/docs
author Pierre-Yves David <pierre-yves.david@ens-lyon.org>
Tue, 07 Mar 2017 14:59:00 +0100
changeset 2057 4c195eb4d2c5
parent 1103 d1ca81f9e458
permissions -rw-r--r--
push: add extra warning about pushing to old server Pushing using old method is slow and racy. We adds warning to point this to the user. We also add inline comment to clarify the function purpose.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
531
b18b00036355 pkg/debian: Debian packaging
Pierre-Yves David <pierre-yves.david@logilab.fr>
parents:
diff changeset
     1
html
1103
d1ca81f9e458 debian: add README to the list of documents shipped with the package.
Faheem Mitha <faheem@faheem.info>
parents: 531
diff changeset
     2
README