diff options
| author |  Stephane Glondu <steph@glondu.net> | 2008-07-28 16:00:07 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2008-07-28 16:00:07 +0200 |
| commit | 3113f65a3dd4bbe1833dcf78fb21abd958dcdb04 (patch) | |
| tree | 93c8d010584cf5dbae68ef8b5976153f9b288dfa | |
| parent | be8dd49cdf08dbeae0d6f36b717a54793418086b (diff) | |
ide/index_urls.txt is not there anymore
| -rwxr-xr-x | debian/rules | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index 1dc43f97..44dac55d 100755 --- a/debian/rules +++ b/debian/rules @@ -96,7 +96,6 @@ install: build cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm cp debian/coqide.desktop debian/coqide/usr/share/applications - cp ide/index_urls.txt debian/coqide/usr/lib/coq/ide/index_urls.txt if [ -e opt-stamp ]; then \ cp debian/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \ cp debian/coqide.1 debian/coqide/usr/share/man/man1/coqide.opt.1; \ |